Coqide: new backtracking code, based on the Backtrack command

 This approach, inspired by ProofGeneral, is *much* simplier than earlier,
 and should be more robust (I hope! feedback of testers is welcome).

 Coqide still continues to send orders like "Rewind 5" for undoing 5 phrases.
 A stack on the coqtop side (in Ide_slave) convert this phrase count to
 labels in the sense of Backtrack, and to abort + depth informations
 concerning proofs.

 We avoid re-entering finished proofs during Rewind by some extra backtracking
 until before these proofs. The amount of extra backtracking is then answered
 by coqtop to coqide. Now:
  - for go_to_insert (the "goto" button), unlike PG, coqide replays
    the extra backtracked zone.
  - for undo_last_step (the "back" button), coqide now leaves the extra
    backtracked zone undone, just like PG. This happens typically when
    undoing a Qed, and this should be the only visible semantical change
    of this patch.

 Two points to check with Pierre C:
  - such a coqtop-side stack mapping labels to opened proofs might be
    interesting to PG, instead of passing lots of info via the prompt and
    computing stuff in emacs.
  - Unlike PG, we allow re-entering inside a module / section, while
    PG retracts to the start of it. Coqide seems to work fine this way, to
    check.

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

2 files changed, 56 insertions, 49 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index 685bfcac3..047a26587 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -47,7 +47,7 @@ val interrupter : (int -> unit) ref
 
 val interp :
   coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Ide_intf.value
-val rewind : coqtop -> int -> unit Ide_intf.value
+val rewind : coqtop -> int -> int Ide_intf.value
 val status : coqtop -> string Ide_intf.value
 val goals : coqtop -> Ide_intf.goals Ide_intf.value
 val inloadpath : coqtop -> string -> bool Ide_intf.value
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 7a714b1d0..e6968c51c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1096,6 +1096,41 @@ object(self)
       Mutex.unlock resetting
     end
 
+  (* Internal method for dialoging with coqtop about a backtrack.
+     The ide's cmd_stack has already been cleared up to the desired point.
+     The [finish] function is used to handle minor differences between
+     [go_to_insert] and [undo_last_step] *)
+
+  method private do_backtrack finish n =
+    (* pop n more commands if coqtop has said so (e.g. for undoing a proof) *)
+    let rec n_pop n =
+      if n = 0 then ()
+      else
+	let phrase = Stack.pop cmd_stack in
+	let stop = input_buffer#get_iter_at_mark phrase.stop in
+        if stop#backward_char#has_tag Tags.Script.comment
+	  then n_pop n
+	  else n_pop (pred n)
+    in
+    match Coq.rewind !mycoqtop n with
+      | Ide_intf.Good n ->
+	n_pop n;
+        sync (fun _ ->
+          let start =
+            if Stack.is_empty cmd_stack then input_buffer#start_iter
+            else input_buffer#get_iter_at_mark (Stack.top cmd_stack).stop in
+	  let stop = self#get_start_of_input in
+          input_buffer#remove_tag Tags.Script.processed ~start ~stop;
+          input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
+          input_buffer#move_mark ~where:start (`NAME "start_of_input");
+          self#show_goals;
+          self#clear_message;
+          finish start) ()
+      | Ide_intf.Fail (l,str) ->
+        sync self#set_message
+          ("Error while backtracking :\n" ^ str ^ "\n" ^
+	   "CoqIDE and coqtop may be out of sync, you may want to use Restart.")
+
   (* backtrack Coq to the phrase preceding iterator [i] *)
   method backtrack_to_no_lock i =
     prerr_endline "Backtracking_to iter starts now.";
@@ -1103,42 +1138,21 @@ object(self)
     (* pop Coq commands until we reach iterator [i] *)
     let rec n_step n =
       if Stack.is_empty cmd_stack then n else
-        let ide_ri = Stack.pop cmd_stack in
-	let stop = input_buffer#get_iter_at_mark ide_ri.stop in
-        if i#compare stop < 0 then
+        let phrase = Stack.top cmd_stack in
+	let stop = input_buffer#get_iter_at_mark phrase.stop in
+        if i#compare stop >= 0 then n
+	else begin
+	  ignore (Stack.pop cmd_stack);
           if stop#backward_char#has_tag Tags.Script.comment
 	  then n_step n
 	  else n_step (succ n)
-        else
-          (Stack.push ide_ri cmd_stack; n)
+	end
     in
     begin
       try
-        match Coq.rewind !mycoqtop (n_step 0) with
-          | Ide_intf.Fail (l,str) ->
-            sync self#set_message
-              ("Error while backtracking :\n" ^ str ^ "\n" ^
-	       "CoqIDE and coqtop may be out of sync," ^
-	       "you may want to use Restart.")
-          | Ide_intf.Good () ->
-            sync (fun _ ->
-              let start =
-                if Stack.is_empty cmd_stack then input_buffer#start_iter
-                else input_buffer#get_iter_at_mark (Stack.top cmd_stack).stop in
-              prerr_endline "Removing (long) processed tag...";
-              input_buffer#remove_tag
-                Tags.Script.processed
-                ~start
-                ~stop:self#get_start_of_input;
-              input_buffer#remove_tag
-                Tags.Script.unjustified
-                ~start
-                ~stop:self#get_start_of_input;
-              prerr_endline "Moving (long) start_of_input...";
-              input_buffer#move_mark ~where:start (`NAME "start_of_input");
-              self#show_goals;
-              self#clear_message)
-              ();
+	self#do_backtrack (fun _ -> ()) (n_step 0);
+	(* We may have backtracked too much: let's replay *)
+	self#process_until_iter_or_error i
       with _ ->
         push_info
 	  ("WARNING: undo failed badly.\n" ^
@@ -1164,24 +1178,17 @@ object(self)
     if Mutex.try_lock coq_may_stop then
       (push_info "Undoing last step...";
        (try
-          let ide_ri = Stack.pop cmd_stack in
-          let start = input_buffer#get_iter_at_mark ide_ri.start in
-	  let stop = input_buffer#get_iter_at_mark ide_ri.stop in
-          let update_input () =
-            prerr_endline "Removing processed tag...";
-            input_buffer#remove_tag Tags.Script.processed ~start ~stop;
-            input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
-            prerr_endline "Moving start_of_input";
-            input_buffer#move_mark ~where:start (`NAME "start_of_input");
-            input_buffer#place_cursor ~where:start;
-            self#recenter_insert;
-            self#show_goals;
-            self#clear_message
-          in
-            if not (stop#backward_char#has_tag Tags.Script.comment) then ignore (Coq.rewind !mycoqtop 1);
-            sync update_input ()
-        with
-          | Stack.Empty -> (* flash_info "Nothing to Undo"*)()
+          let phrase = Stack.pop cmd_stack in
+	  let stop = input_buffer#get_iter_at_mark phrase.stop in
+	  let count =
+	    if stop#backward_char#has_tag Tags.Script.comment then 0 else 1
+	  in
+	  let finish where =
+	    input_buffer#place_cursor ~where;
+	    self#recenter_insert;
+	  in
+	  self#do_backtrack finish count
+        with Stack.Empty -> ()
        );
        pop_info ();
        Mutex.unlock coq_may_stop)