diff options
| -rw-r--r-- | checker/check_stat.ml | 2 | ||||
| -rw-r--r-- | lib/errors.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 10 |
3 files changed, 11 insertions, 3 deletions
diff --git a/checker/check_stat.ml b/checker/check_stat.ml index a26c93a30..a63705adc 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -18,7 +18,7 @@ let print_memory_stat () = if !memory_stat then begin Format.printf "total heap size = %d kbytes\n" (CObj.heap_size_kb ()); Format.print_newline(); - flush_all() + Format.print_flush() end let output_context = ref false diff --git a/lib/errors.ml b/lib/errors.ml index 8982dde14..1459141d1 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -144,5 +144,5 @@ let handled e = let fatal_error info anomaly = let msg = info ++ fnl () in pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg; - flush_all (); + Format.pp_print_flush !Pp_control.err_ft (); exit (if anomaly then 129 else 1) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index c7a639803..1fe30217d 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -345,13 +345,21 @@ let feed_emacs = function | _ -> () *) +(* Flush in a compatible order with 8.5 *) +(* This mimics the semantics of the old Pp.flush_all *) +let loop_flush_all () = + Pervasives.flush stderr; + Pervasives.flush stdout; + Format.pp_print_flush !Pp_control.std_ft (); + Format.pp_print_flush !Pp_control.err_ft () + let rec loop () = Sys.catch_break true; if !Flags.print_emacs then Vernacentries.qed_display_script := false; Flags.coqtop_ui := true; try reset_input_buffer stdin top_buffer; - while true do do_vernac(); flush_all() done + while true do do_vernac(); loop_flush_all () done with | Errors.Drop -> () | Errors.Quit -> exit 0 |