Automatic backtracking if locked zone is edited

That is pretty tricky, and is not as nice I would like
for to_process text (that is still considered as locked).

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

4 files changed, 47 insertions, 24 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 66e932608..534dd504d 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -72,6 +72,7 @@ let log msg : unit task =
 class type ops =
 object
   method go_to_insert : unit task
+  method go_to_mark : GText.mark -> unit task
   method tactic_wizard : string list -> unit task
   method process_next_phrase : unit task
   method process_until_end_or_error : unit task
@@ -405,12 +406,12 @@ object(self)
       None, List.rev (Searchstack.to_list cmd_stack)
 
   (** Wrapper around the raw undo command *)
-  method private backtrack_until until =
+  method private backtrack_until ?(move_insert=true) until =
     let opening () =
       push_info "Coq is undoing" in
     let conclusion () =
       pop_info ();
-      buffer#place_cursor ~where:self#get_start_of_input;
+      if move_insert then buffer#place_cursor ~where:self#get_start_of_input;
       self#show_goals in
     let cleanup n l =
       for i = 1 to n do ignore(Searchstack.pop cmd_stack) done;
@@ -437,9 +438,9 @@ object(self)
     in
       undo until)
 
-  method private backtrack_to_iter iter =
+  method private backtrack_to_iter ?move_insert iter =
     let until _ _ _ stop = iter#compare (buffer#get_iter_at_mark stop) >= 0 in
-    self#backtrack_until until
+    self#backtrack_until ?move_insert until
 
   method handle_failure (safe_id, (loc : (int * int) option), msg) =
     if loc <> None then messages#push Error "Fixme LOC";
@@ -466,7 +467,16 @@ object(self)
     let point = self#get_insert in
     if point#compare self#get_start_of_input >= 0
     then self#process_until_iter point
-    else self#backtrack_to_iter point)
+    else self#backtrack_to_iter ~move_insert:false point)
+
+  method go_to_mark m =
+    Coq.bind (Coq.return ()) (fun () ->
+    messages#clear;
+    let point = buffer#get_iter_at_mark m in
+    if point#compare self#get_start_of_input >= 0
+    then self#process_until_iter point
+    else self#backtrack_to_iter ~move_insert:false point)
+
 
   method tactic_wizard l =
     let insert_phrase phrase tag =
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 37daaf307..d286ad3d1 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -11,6 +11,7 @@ open Coq
 class type ops =
 object
   method go_to_insert : unit task
+  method go_to_mark : GText.mark -> unit task
   method tactic_wizard : string list -> unit task
   method process_next_phrase : unit task
   method process_until_end_or_error : unit task
diff --git a/ide/session.ml b/ide/session.ml
index bed0747f3..e001efc46 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -78,16 +78,17 @@ let create_script coqtop source_buffer =
   point. At the end, the zone between the mark and the cursor is to be
   untagged and then retagged. *)
 
-let set_buffer_handlers buffer script =
+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 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 a #insert happens in the locked zone, we discard it.
-        Other solution: always use #insert_interactive and similar *)
-    let () =
-      let start = get_start () in
-      if it#compare start < 0 then GtkSignal.stop_emit ()
-    in
     if String.length s > 1 then
       let () = Minilib.log "insert_text: Placing cursor" in
       let () = buffer#place_cursor ~where:it in
@@ -95,20 +96,31 @@ let set_buffer_handlers buffer script =
         let () = Minilib.log "insert_text: Recentering" in
         script#recenter_insert
   in
+  let begin_action_did_not_cancel = ref true in
   let begin_action_cb () =
+    begin_action_did_not_cancel := false;
     (* We remove any error red zone, and place the [prev_insert] mark *)
-    let where = get_insert () in
-    let () = buffer#move_mark (`NAME "prev_insert") ~where in
-    let start = get_start () 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
+    let cleanup () =
+      begin_action_did_not_cancel := true;
+      let where = get_insert () in
+      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 0 <= ins#compare start then Sentence.tag_on_insert buffer
+    if !begin_action_did_not_cancel &&
+       0 <= ins#compare start then Sentence.tag_on_insert buffer
   in
   let mark_set_cb it m =
     let ins = get_insert () in
@@ -150,7 +162,6 @@ let create file coqtop_args =
   let reset () = Coq.reset_coqtop coqtop in
   let buffer = create_buffer () in
   let script = create_script coqtop buffer in
-  let _ = set_buffer_handlers (buffer :> GText.buffer) script in
   let proof = create_proof () in
   let messages = create_messages () in
   let command = new Wg_Command.command_window coqtop ~mark_as_broken:(fun _ -> ()) ~mark_as_processed:(fun _ -> ()) ~cur_state:(fun () -> Obj.magic 0) in
@@ -159,6 +170,7 @@ let create file coqtop_args =
   let _ = fops#update_stats in
   let cops =
     new CoqOps.coqops script proof messages coqtop (fun () -> fops#filename) in
+  let _ = set_buffer_handlers (buffer :> GText.buffer) script cops coqtop in
   let _ = Coq.set_reset_handler coqtop cops#handle_reset_initial in
   let _ = Coq.init_coqtop coqtop cops#initialize in
   {
diff --git a/ide/tags.ml b/ide/tags.ml
index e668616bf..a91905dcd 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -22,9 +22,9 @@ struct
   let comment_sentence = make_tag table ~name:"comment_sentence" []
   let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]
   let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND "#FFCCCC"]
-  let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color ;`EDITABLE false]
-  let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color;`EDITABLE false]
-  let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold";`EDITABLE false]
+  let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color]
+  let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color]
+  let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"]
   let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]
   let sentence = make_tag table ~name:"sentence" []
   let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *)