minor fixes

src/driver/driver.ml

@@ -173,16 +173,10 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
         let td = create_meta m (List.map convert al) in
         add_meta th td meta
   in
-  let add_local th (loc,rule) =
-    try add_local th rule with e -> raise (Loc.Located (loc,e))
-  in
+  let add_local th (loc,rule) = Loc.try2 ~loc add_local th rule in
   let add_theory { thr_name = (loc,q); thr_rules = trl } =
     let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
-    let th =
-      try Env.read_theory env f id
-      with e when not (Debug.test_flag Debug.stack_trace) ->
-        raise (Loc.Located (loc,e))
-    in
+    let th = Loc.try3 ~loc Env.read_theory env f id in
     qualid := q;
     List.iter (add_local th) trl
   in

src/printer/gappa.ml

@@ -66,8 +66,7 @@ let incremental_pat_match env holes =
         end
     | PatApp (sp,ss,sl,pl), Tapp (ls,tl) ->
         if List.length pl <> List.length tl then raise Not_found;
-        let th = try Env.read_theory env sp ss
-          with Env.TheoryNotFound _ -> raise Not_found in
+        let th = Env.read_theory env sp ss in
         let s = ns_find_ls th.th_export sl in
         if not (ls_equal s ls) then raise Not_found;
         List.iter2 aux pl tl

src/printer/mathematica.ml

@@ -37,8 +37,7 @@ let incremental_pat_match env holes =
         end
     | PatApp (sp,ss,sl,pl), Tapp (ls,tl) ->
         if List.length pl <> List.length tl then raise Not_found;
-        let th = try Env.read_theory env sp ss
-          with Env.TheoryNotFound _ -> raise Not_found in
+        let th = Env.read_theory env sp ss in
         let s = ns_find_ls th.th_export sl in
         if not (ls_equal s ls) then raise Not_found;
         List.iter2 aux pl tl

src/tools/why3execute.ml

@@ -43,11 +43,13 @@ let () =
   if !opt_file = None then Whyconf.Args.exit_with_usage option_list usage_msg
 
 let do_input f =
-  let fname, cin =
-    match f with
-    | "-" -> "stdin", stdin
-    | f   -> f, open_in f in
-  let mm, _thm = Env.read_channel Mlw_module.mlw_language env fname cin in
+  let format = !opt_parser in
+  let mm, _thm = match f with
+    | "-" ->
+        Env.read_channel Mlw_module.mlw_language ?format env "stdin" stdin
+    | file ->
+        Env.read_file Mlw_module.mlw_language ?format env file
+  in
   let do_exec (mid,name) =
     let m = try Mstr.find mid mm with Not_found ->
       eprintf "Module '%s' not found.@." mid;

src/tools/why3extract.ml

@@ -173,25 +173,24 @@ let do_extract_module_from fname mm thm (tname,_,t) =
 
 let do_local_extract fname cin tlist =
   let env = opt_driver.Mlw_driver.drv_env in
-  if !opt_parser = Some "whyml" || Filename.check_suffix fname ".mlw" then begin
-    let mm, thm = Env.read_channel Mlw_module.mlw_language env fname cin in
-    if Queue.is_empty tlist then begin
-      let do_m t m thm =
-        do_extract_module ~fname m; Mstr.remove t thm in
+  let format = !opt_parser in
+  try
+    let mm, thm =
+      Env.read_channel ?format Mlw_module.mlw_language env fname cin in
+    if Queue.is_empty tlist then
+      let do_m t m thm = do_extract_module ~fname m; Mstr.remove t thm in
       let thm = Mstr.fold do_m mm thm in
       Mstr.iter (fun _ th -> do_extract_theory ~fname th) thm
-    end else
+    else
       Queue.iter (do_extract_module_from fname mm thm) tlist
-  end else begin
-    let m = Env.read_channel ?format:!opt_parser
-      Env.base_language env fname cin in
+  with Env.InvalidFormat _ ->
+    let m = Env.read_channel ?format Env.base_language env fname cin in
     if Queue.is_empty tlist then
       let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
       let do_th _ (_,th) = do_extract_theory ~fname th in
       Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
     else
       Queue.iter (do_extract_theory_from fname m) tlist
-  end
 
 let do_input = function
   | None, tlist ->

src/tools/why3prove.ml

@@ -344,15 +344,14 @@ let do_input env drv = function
   | None, tlist ->
       Queue.iter (do_global_theory env drv) tlist
   | Some f, tlist ->
-      let fname, cin = match f with
-        | "-" -> "stdin", stdin
-        | f   -> f, open_in f
+      let format = !opt_parser in
+      let fname, m = match f with
+        | "-" -> "stdin",
+            Env.read_channel Env.base_language ?format env "stdin" stdin
+        | fname -> fname,
+            Env.read_file Env.base_language ?format env fname
       in
-      let m = Env.read_channel ?format:!opt_parser
-        Env.base_language env fname cin in
-      close_in cin;
-      if Debug.test_flag Typing.debug_type_only then
-        ()
+      if Debug.test_flag Typing.debug_type_only then ()
       else
         if Queue.is_empty tlist then
           let glist = Queue.create () in