Skip to content

Commit

Permalink
Fix coq#17753 coqtop output is sometimes incorrecty ordered.
Browse files Browse the repository at this point in the history
Which seems to cause [this PG
bug](ProofGeneral/PG#429 (comment)).
  • Loading branch information
Matafou committed Jun 20, 2023
1 parent 8f100d7 commit 3f970da
Showing 1 changed file with 7 additions and 4 deletions.
11 changes: 7 additions & 4 deletions toplevel/coqloop.ml
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,9 @@ let print_emacs = ref false
let top_stderr x =
Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x

let top_std x =
Format.fprintf !Topfmt.std_ft "@[%a@]%!" pp_with x

(* A buffer for the character read from a channel. We store the command
* entered to be able to report errors without pretty-printing. *)

Expand Down Expand Up @@ -59,7 +62,7 @@ let prompt_char doc ic ibuf count =
| ll::_ -> Int.equal ibuf.len ll
| [] -> Int.equal ibuf.len 0
in
if bol && not !print_emacs then top_stderr (str (ibuf.prompt doc));
if bol && not !print_emacs then top_std (str (ibuf.prompt doc));
try
let c = input_char ic in
if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
Expand Down Expand Up @@ -331,9 +334,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
(* This mimics the semantics of the old Pp.flush_all *)
let loop_flush_all () =
flush stderr;
Format.pp_print_flush !Topfmt.err_ft ();
flush stdout;
Format.pp_print_flush !Topfmt.std_ft ();
Format.pp_print_flush !Topfmt.err_ft ()
Format.pp_print_flush !Topfmt.std_ft ()

(* Goal equality heuristic. *)
let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2
Expand Down Expand Up @@ -495,7 +498,7 @@ let rec vernac_loop ~state =
let open Vernac.State in
loop_flush_all ();
top_stderr (fnl());
if !print_emacs then top_stderr (str (top_buffer.prompt state.doc));
if !print_emacs then top_std (str (top_buffer.prompt state.doc));
resynch_buffer top_buffer;
let state, drop = read_and_execute ~state in
if drop then state else (vernac_loop [@ocaml.tailcall]) ~state
Expand Down

0 comments on commit 3f970da

Please sign in to comment.