From 2e0e2d662421c5c1ec3415da9ca94054e0cc2898 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 7 Jun 2016 10:50:55 +0200
Subject: Fix for bug #4784

We revert the change of flushing strategy in the toplevel.

PR #179 introduced a different flushing in toplevel, but it creates
problems as new lines appear when Set Printing Width is large and proof
general complains, see bugzilla#4784. The use of `flush_all` also
produces missing output.

IMO, this is a pitfall of the current setup, in particular, `Format` is
used without enclosing expressions in top-level boxes, as required. This
results in undefined behavior and fragile printing such as this bug
exemplifies.

Test suite passes.
---
 toplevel/coqloop.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index c8879963e5..c7a6398035 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -328,7 +328,7 @@ let do_vernac () =
         Format.set_formatter_out_channel stdout;
         let msg = print_toplevel_error any ++ fnl () in
         pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg;
-        flush_all ()
+        Format.pp_print_flush !Pp_control.std_ft ()
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
-- 
cgit v1.2.3