diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-07 16:28:27 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-14 19:31:10 +0200 |
commit | e129410314b2e4e6ed7dc2c0814332a67444b01a (patch) | |
tree | 6b1b83f0b9dcd583071fb6f4f475b5add0815d9c /toplevel | |
parent | 2e0e2d662421c5c1ec3415da9ca94054e0cc2898 (diff) |
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.
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/coqloop.ml | 10 |
1 files changed, 9 insertions, 1 deletions
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 |