diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-09-28 17:00:09 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-10-22 11:57:58 +0200 |
| commit | cc2778c3310a75585c00f0eb659ddde7aee2944a (patch) | |
| tree | 8a0a403eb33401748a6c0d4c67465661270e8729 | |
| parent | 9f8714f4cd3fb59ce38afee48caf081db1919c0c (diff) | |
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.
| -rw-r--r-- | ide/session.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/session.ml b/ide/session.ml index 168ddd4df..711111139 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -111,10 +111,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 @@ -127,7 +127,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 |