From d907342e31930eb2b8af7c9cc12bd0ddc7c00709 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 28 Sep 2016 17:00:09 +0200 Subject: Do not stop propagation of signals when Coq is busy (bug #3941). When inserting a character in an already processed buffer, a message is sent to Coq so that the proof is backtracked and the character is inserted. If a second character is inserted while Coq is still busy with the first message, the action is canceled, but the signal is no longer dropped so that the second character is properly inserted. --- ide/session.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'ide/session.ml') diff --git a/ide/session.ml b/ide/session.ml index e99833760..fc6340d28 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -108,10 +108,10 @@ let set_buffer_handlers let id = ref 0 in fun () -> incr id; !id in let running_action = ref None in - let cancel_signal reason = + let cancel_signal ?(stop_emit=true) reason = Minilib.log ("user_action cancelled: "^reason); action_was_cancelled := true; - GtkSignal.stop_emit () in + if stop_emit then GtkSignal.stop_emit () in let del_mark () = try buffer#delete_mark (`NAME "target") with GText.No_such_mark _ -> () in @@ -124,7 +124,7 @@ let set_buffer_handlers fun () -> (* If Coq is busy due to the current action, we don't cancel *) match !running_action with | Some aid when aid = action -> () - | _ -> cancel_signal "Coq busy" in + | _ -> cancel_signal ~stop_emit:false "Coq busy" in Coq.try_grab coqtop action fallback in let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in -- cgit v1.2.3