diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-07 10:50:55 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-06-14 19:31:10 +0200 |
| commit | 2e0e2d662421c5c1ec3415da9ca94054e0cc2898 (patch) | |
| tree | 644e2a515ce8bbbfe24d51836a48c803aeabcffb /toplevel | |
| parent | 4a5b6f10b55597e0a0d27ec34fa4f914cfcbc6e8 (diff) | |
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.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqloop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index c8879963e..c7a639803 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. |