diff options
| author | ppedrot | 2012-06-02 13:52:31 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-02 13:52:31 +0000 |
| commit | de9e40dc84d1e4cfc201eb196659d6b04a7012ec (patch) | |
| tree | 6a24553f3391adeb45a9c7e839711226faed4c1a /toplevel | |
| parent | a92a0d051b987ba996905ccd4ce7ee3a5feb41c1 (diff) | |
Flushing formatters before program exit.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15415 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 14 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
2 files changed, 10 insertions, 6 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a60e74f16b..a486de2e2e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -18,6 +18,11 @@ open States open Toplevel open Coqinit +let () = at_exit flush_all + +let fatal_error info = + pperrnl info; flush_all (); exit 1 + let get_version_date () = try let coqlib = Envars.coqlib Errors.error in @@ -309,9 +314,9 @@ let parse_args arglist = try Stream.empty s; exit 1 with Stream.Failure -> - pperrnl (Errors.print e); exit 1 + fatal_error (Errors.print e) end - | e -> begin pperrnl (Errors.print e); exit 1 end + | e -> fatal_error (Errors.print e) let init arglist = Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) @@ -344,9 +349,8 @@ let init arglist = outputstate () with e -> flush_all(); - if not !batch_mode then pperrnl - (str "Error during initialization:" ++ fnl () ++ Toplevel.print_toplevel_error e); - exit 1 + if not !batch_mode then + fatal_error (str "Error during initialization:" ++ fnl () ++ Toplevel.print_toplevel_error e) end; if !batch_mode then (flush_all(); diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d6178cd624..ac3dd39cbf 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -357,7 +357,7 @@ let compile verbosely f = if !Flags.xml_export then !xml_start_library (); let _ = load_vernac verbosely long_f_dot_v in if Pfedit.get_all_proof_names () <> [] then - (pperrnl (str "Error: There are pending proofs"); exit 1); + (pperrnl (str "Error: There are pending proofs"); flush_all (); exit 1); if !Flags.xml_export then !xml_end_library (); Dumpglob.end_dump_glob (); Library.save_library_to ldir (long_f_dot_v ^ "o") |