From 0b48c57d705873d142cb4b19f959d1e7fab116c8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 1 Apr 2018 02:57:02 +0200 Subject: [toplevel] Protect goal printing better wrt Break [fixes #7142] When interrupting goal printing, we should continue the loop with the newly generated state, that should help avoiding synchronization problems as in #7142. Fixes #7142. --- toplevel/coqloop.ml | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 64d839f18..ef519905d 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -325,6 +325,24 @@ let cproof p1 p2 = let drop_last_doc = ref None +(* We try to behave better when goal printing raises an exception + [usually Ctrl-C] + + This is mostly a hack as we should protect printing in a more + generic way, but that'll do for now *) +let top_goal_print oldp newp = + try + let proof_changed = not (Option.equal cproof oldp newp) in + let print_goals = not !Flags.quiet && + proof_changed && Proof_global.there_are_pending_proofs () in + if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()) + with + | exn -> + let (e, info) = CErrors.push exn in + let loc = Loc.get_loc info in + let msg = CErrors.iprint (e, info) in + TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer + (* Careful to keep this loop tail-rec *) let rec vernac_loop ~state = let open CAst in @@ -346,10 +364,7 @@ let rec vernac_loop ~state = else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state) | {v=VernacControl c; loc} -> let nstate = Vernac.process_expr ~state (make ?loc c) in - let proof_changed = not (Option.equal cproof nstate.proof state.proof) in - let print_goals = not !Flags.quiet && - proof_changed && Proof_global.there_are_pending_proofs () in - if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); + top_goal_print state.proof nstate.proof; vernac_loop ~state:nstate with | Stm.End_of_input -> -- cgit v1.2.3