Flushing formatters before program exit.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15415 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 25 insertions, 17 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 848fd22f4..53c059eb3 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -16,6 +16,11 @@ open Names
 open Term
 open Check
 
+let () = at_exit flush_all
+
+let fatal_error info =
+  pperrnl info; flush_all (); exit 1
+
 let coq_root = id_of_string "Coq"
 let parse_dir s =
   let len = String.length s in
@@ -292,7 +297,7 @@ let parse_args argv =
 
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
-	(pperrnl (str ("Directory '"^s^"' does not exist")); exit 1);
+	fatal_error (str ("Directory '"^s^"' does not exist"));
       Flags.coqlib := s;
       Flags.coqlib_spec := true;
       parse rem
@@ -332,7 +337,7 @@ let parse_args argv =
         Flags.make_silent true; parse rem
 
     | s :: _ when s<>"" && s.[0]='-' ->
-        pperrnl (str "Unknown option " ++ str s); exit 1
+        fatal_error (str "Unknown option " ++ str s)
     | s :: rem ->  add_compile s; parse rem
   in
   try
@@ -342,9 +347,9 @@ let parse_args argv =
 	try
 	  Stream.empty s; exit 1
 	with Stream.Failure ->
-	  pperrnl (explain_exn e); exit 1
+	  fatal_error (explain_exn e)
       end
-    | e -> begin pperrnl (explain_exn e); exit 1 end
+    | e -> begin fatal_error (explain_exn e) end
 
 
 (* To prevent from doing the initialization twice *)
@@ -360,9 +365,7 @@ let init_with_argv argv =
       init_load_path ();
       engage ();
     with e ->
-      flush_all();
-      pperrnl (str "Error during initialization :" ++ (explain_exn e));
-      exit 1
+      fatal_error (str "Error during initialization :" ++ (explain_exn e))
   end
 
 let init() = init_with_argv Sys.argv
@@ -372,8 +375,6 @@ let run () =
     compile_files ();
     flush_all()
   with e ->
-    (Pp.ppnl(explain_exn e);
-    flush_all();
-    exit 1)
+    fatal_error (explain_exn e)
 
 let start () = init(); run(); Check_stat.stats(); exit 0
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 0ec4ea4c9..f64f932e2 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -322,7 +322,9 @@ let pperrnl   x = ppnl_with !err_ft x
 let message   s = ppnl      (str s)
 let warning   x = warning_with !err_ft x
 let pp_flush  x = Format.pp_print_flush !std_ft x
-let flush_all() = flush stderr; flush stdout; pp_flush()
+let pperr_flush x = Format.pp_print_flush !err_ft x
+let flush_all () =
+  flush stderr; flush stdout; pp_flush (); pperr_flush ()
 
 (* pretty printing functions WITH FLUSH *)
 let msg x = msg_with !std_ft x
diff --git a/lib/pp.mli b/lib/pp.mli
index 58a5171d3..6dcbc0411 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -149,6 +149,7 @@ val pp : std_ppcmds -> unit
 val ppnl : std_ppcmds -> unit
 val pperr : std_ppcmds -> unit
 val pperrnl : std_ppcmds -> unit
+val pperr_flush : unit -> unit
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a60e74f16..a486de2e2 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 d6178cd62..ac3dd39cb 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")