CoqIDE: fixed detection of edits in the locked zone

Trying to understand if the edit concernes the processed zone
from the begin_user_action callback was a bad idea, the callback
cannot reliably know where the edit takes place (E.g. insert mark
means nothing: one can copy from the insert point but paste elsewhere).

The callbacks delete_range and insert_text do know where the edit is and
can ask coq to backtrack if needed.  If coq is busy, the user action is
cancelled (the locked zone cannot be unlocked).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16715 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 40 insertions, 34 deletions

diff --git a/ide/session.ml b/ide/session.ml
index e001efc46..e9d4b48ac 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -81,47 +81,52 @@ let create_script coqtop source_buffer =
 let set_buffer_handlers
   (buffer : GText.buffer) script (coqops : CoqOps.ops) coqtop
 =
-  let call_coq f =
-    let abort () =
-      Minilib.log ("Coq busy, discarding query");
-      GtkSignal.stop_emit () in
-    Coq.try_grab coqtop f abort in
+  let action_was_cancelled = ref true in
+  let cancel_signal reason =
+    Minilib.log ("user_action cancelled: "^reason);
+    action_was_cancelled := true;
+    GtkSignal.stop_emit () in
+  let del_mark () =
+    try buffer#delete_mark (`NAME "target")
+    with GText.No_such_mark _ -> () in
+  let add_mark it = del_mark (); buffer#create_mark ~name:"target" it in
+  let call_coq_or_cancel_action f =
+    Coq.try_grab coqtop f (fun () -> cancel_signal "Coq busy") in
   let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in
   let get_insert () = buffer#get_iter_at_mark `INSERT in
-  let insert_cb it s =
-    if String.length s > 1 then
-      let () = Minilib.log "insert_text: Placing cursor" in
-      let () = buffer#place_cursor ~where:it in
-      if String.contains s '\n' then
-        let () = Minilib.log "insert_text: Recentering" in
-        script#recenter_insert
-  in
-  let begin_action_did_not_cancel = ref true in
+  let insert_cb it s = if String.length s = 0 then () else begin
+    Minilib.log ("insert_cb " ^ string_of_int it#offset);
+    let text_mark = add_mark it in
+    if it#has_tag Tags.Script.to_process then
+      cancel_signal "Altering to the script being processed in not implemented"
+    else if it#has_tag Tags.Script.processed then
+      call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
+    end in
+  let delete_cb ~start ~stop =
+    Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset);
+    let min_iter = if start#compare stop < 0 then start else stop in
+    let text_mark = add_mark min_iter in
+    if min_iter#has_tag Tags.Script.to_process then
+      cancel_signal "Altering to the script being processed in not implemented"
+    else if min_iter#has_tag Tags.Script.processed then
+      call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark)) in
   let begin_action_cb () =
-    begin_action_did_not_cancel := false;
-    (* We remove any error red zone, and place the [prev_insert] mark *)
-    let cleanup () =
-      begin_action_did_not_cancel := true;
-      let where = get_insert () in
+    action_was_cancelled := false;
+    let where = get_insert () in
+    buffer#move_mark (`NAME "prev_insert") ~where in
+  let end_action_cb () =
+    Minilib.log "end_action_cb";
+    if not !action_was_cancelled then begin
+      Minilib.log "cleanup tags";
       let start = get_start () in
-      let () = buffer#move_mark (`NAME "prev_insert") ~where in
       let stop = buffer#end_iter in
       buffer#remove_tag Tags.Script.error ~start ~stop;
       buffer#remove_tag Tags.Script.error_bg ~start ~stop;
-      buffer#remove_tag Tags.Script.tooltip ~start ~stop in
-    if (get_insert ())#has_tag Tags.Script.to_process then
-      GtkSignal.stop_emit ()
-    else if (get_insert ())#compare (get_start()) < 0 then
-      call_coq (Coq.seq coqops#go_to_insert (Coq.lift cleanup))
-    else
-      cleanup ()
-  in
-  let end_action_cb () =
-    let start = get_start () in
-    let ins = get_insert () in
-    if !begin_action_did_not_cancel &&
-       0 <= ins#compare start then Sentence.tag_on_insert buffer
-  in
+      buffer#remove_tag Tags.Script.tooltip ~start ~stop;
+      buffer#remove_tag Tags.Script.processed ~start ~stop;
+      buffer#remove_tag Tags.Script.to_process ~start ~stop;
+      Sentence.tag_on_insert buffer;
+    end in
   let mark_set_cb it m =
     let ins = get_insert () in
     let line = ins#line + 1 in
@@ -135,6 +140,7 @@ let set_buffer_handlers
   in
   (** Pluging callbacks *)
   let _ = buffer#connect#insert_text ~callback:insert_cb in
+  let _ = buffer#connect#delete_range ~callback:delete_cb in
   let _ = buffer#connect#begin_user_action ~callback:begin_action_cb in
   let _ = buffer#connect#end_user_action ~callback:end_action_cb in
   let _ = buffer#connect#after#mark_set ~callback:mark_set_cb in