From e129410314b2e4e6ed7dc2c0814332a67444b01a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 7 Jun 2016 16:28:27 +0200
Subject: Preventive compatibility fixes for flushing.

In pre 8.6, `Pp` provided its own reimplementation of
`Pervasives.flush_all`, with different semantics.

Unfortunately, with the removal of `Pp.flush_all` in #179, a couple of
points were silently switched to the `Pervasives` version, which may
lead to some subtle printing differences.

As a preventive measure, we restore the same semantics for these parts
of the codebase.

Note that we don't re-introduce Coq's `flush_all` for several reasons:

- Consumers of the logging API should not mess with flushing and
  Formatters as this is backend dependent (i.e: when in IDEs).

  Use of `Format` should be fully encapsulated if we want some hope of
  IDEs taking full control.

- As used, the old semantics of `flush_all` were fragile.
---
 toplevel/coqloop.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index c7a6398035..1fe30217dd 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
-- 
cgit v1.2.3