Reporting when an error occurs at initialization time.

Done by simplifying the three "try" liable to be caught at
initialization time into one and by ensuring that the remaining one
reports about being in initialization phase.

1 files changed, 16 insertions, 20 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e60382f2c..d497789a6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -489,28 +489,24 @@ let init_toplevel arglist =
         let iload_path = build_load_path opts in
         let require_libs = require_libs opts in
         let stm_options = opts.stm_flags in
-        try
-          let open Vernac.State in
-          let doc, sid =
-            Stm.(new_doc
-                   { doc_type = Interactive opts.toplevel_name;
-                     iload_path; require_libs; stm_options;
-                   }) in
-          let state = { doc; sid; proof = None; time = opts.time } in
-          Some (load_init_vernaculars opts ~state), opts
-        with any -> flush_all(); fatal_error_exn any
+        let open Vernac.State in
+        let doc, sid =
+          Stm.(new_doc
+                 { doc_type = Interactive opts.toplevel_name;
+                   iload_path; require_libs; stm_options;
+                 }) in
+        let state = { doc; sid; proof = None; time = opts.time } in
+        Some (load_init_vernaculars opts ~state), opts
       (* Non interactive: we perform a sequence of compilation steps *)
       end else begin
-        try
-          compile_files opts;
-          (* Careful this will modify the load-path and state so after
-             this point some stuff may not be safe anymore. *)
-          do_vio opts;
-          (* Allow the user to output an arbitrary state *)
-          outputstate opts;
-          None, opts
-        with any -> flush_all(); fatal_error_exn any
-      end;
+        compile_files opts;
+        (* Careful this will modify the load-path and state so after
+           this point some stuff may not be safe anymore. *)
+        do_vio opts;
+        (* Allow the user to output an arbitrary state *)
+        outputstate opts;
+        None, opts
+    end;
     with any ->
       flush_all();
       let extra = Some (str "Error during initialization: ") in