Deport the backtracking code out of the ide

Backtracking code now lies entirely into ide/coq.ml. Datatypes have been
tweaked to easen the separation to come.

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

3 files changed, 200 insertions, 234 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 67cf70a3b..3dc3e1431 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -367,8 +367,12 @@ type reset_status =
   | ResetAtSegmentStart of Names.identifier
   | ResetAtRegisteredObject of reset_mark
 
-type reset_info = reset_status * undo_info * bool ref
-
+type reset_info = {
+  status : reset_status;
+  proofs : identifier list;
+  loc_ast : Util.loc * Vernacexpr.vernac_expr;
+  mutable section : bool;
+}
 
 let reset_mark id = match Lib.has_top_frozen_state () with
   | Some sp -> 
@@ -376,28 +380,32 @@ let reset_mark id = match Lib.has_top_frozen_state () with
       ResetToState sp
   | None -> ResetToId id
 
-let compute_reset_info = function 
-  | VernacBeginSection id 
-  | VernacDefineModule (_,id, _, _, _) 
-  | VernacDeclareModule (_,id, _, _)
-  | VernacDeclareModuleType (id, _, _, _) ->
-      ResetAtSegmentStart (snd id), undo_info(), ref true
-
-  | VernacDefinition (_, (_,id), DefineBody _, _)
-  | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
-  | VernacInductive (_,_, (((_,(_,id)),_,_,_,_),_) :: _) ->
-      ResetAtRegisteredObject (reset_mark id), undo_info(), ref true
-
-  | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true
-  | VernacEndSegment _ -> NoReset, undo_info(), ref true
-
-  | com when is_vernac_tactic_command com -> NoReset, undo_info(), ref true
-  | _ ->
-      (match Lib.has_top_frozen_state () with
-      | Some sp -> 
-	  prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
-	  ResetAtRegisteredObject (ResetToState sp)
-      | None -> NoReset), undo_info(), ref true
+let compute_reset_info loc_ast = 
+  let status = match snd loc_ast with
+    | VernacBeginSection id 
+    | VernacDefineModule (_,id, _, _, _) 
+    | VernacDeclareModule (_,id, _, _)
+    | VernacDeclareModuleType (id, _, _, _) ->
+        ResetAtSegmentStart (snd id)
+    | VernacDefinition (_, (_,id), DefineBody _, _)
+    | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
+    | VernacInductive (_,_, (((_,(_,id)),_,_,_,_),_) :: _) ->
+        ResetAtRegisteredObject (reset_mark id)
+    | com when is_vernac_proof_ending_command com -> NoReset
+    | VernacEndSegment _ -> NoReset
+    | com when is_vernac_tactic_command com -> NoReset
+    | _ ->
+        (match Lib.has_top_frozen_state () with
+           | Some sp -> 
+               prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
+               ResetAtRegisteredObject (ResetToState sp)
+           | None -> NoReset)
+  in
+  { status = status;
+    proofs = Pfedit.get_all_proof_names ();
+    loc_ast = loc_ast; 
+    section = true;
+  }
 
 let reset_initial () =
   prerr_endline "Reset initial called"; flush stderr;
@@ -442,13 +450,13 @@ let interp_with_options verbosely options s =
 	if not (is_vernac_goal_printing_command vernac) then
 	  (* Verbose if in small step forward and not a tactic *)
 	  Flags.make_silent (not verbosely);
-	let reset_info = compute_reset_info vernac in
+	let reset_info = compute_reset_info last in
 	List.iter (fun (set_option,_) -> raw_interp set_option) options;
 	raw_interp s;
 	Flags.make_silent true;
 	List.iter (fun (_,unset_option) -> raw_interp unset_option) options;
 	prerr_endline ("...Done with interp of : "^s);
-	reset_info,last
+	reset_info
 
 let interp verbosely phrase =
   interp_with_options verbosely (make_option_commands ()) phrase
@@ -458,46 +466,6 @@ let interp_and_replace s =
   let msg = read_stdout () in
   result,msg
 
-type bktk_info = { start : GText.mark;
-                   stop : GText.mark;
-                   state_num : int;
-                   pending_proofs : string list;
-                   proof_stack_depth : int;
-}
-
-let record_interp cmd_stk start_of_sentence end_of_sentence (sn,pp,psd) =
-  Stack.push { start = start_of_sentence;
-               stop = end_of_sentence;
-               state_num = sn;
-               pending_proofs = pp;
-               proof_stack_depth = psd;
-  } cmd_stk
-
-let backtrack cmd_stack stop_cond =
-  if Stack.is_empty cmd_stack then
-    reset_initial () (* reset coq *)
-  else try
-    let current = Stack.top cmd_stack in
-    while not (stop_cond (Stack.top cmd_stack).stop) do
-      ignore (Stack.pop cmd_stack)
-    done;
-    let target = Stack.top cmd_stack in
-    if current != target then
-      let rst = target.state_num in
-      let undo = target.proof_stack_depth in
-      let abrt = List.fold_left
-                   (fun acc e -> if List.mem e target.pending_proofs then acc else succ acc)
-                   0 current.pending_proofs
-      in
-      raw_interp (Printf.sprintf "Backtrack %d %d %d.\n" rst undo abrt)
-      else ()
-  with Stack.Empty -> reset_initial () (* might as well reset coq ... *)
-
-type tried_tactic =
-  | Interrupted
-  | Success of int (* nb of goals after *)
-  | Failed
-
 let rec is_pervasive_exn = function
   | Out_of_memory | Stack_overflow | Sys.Break -> true
   | Error_in_file (_,_,e) -> is_pervasive_exn e
@@ -539,6 +507,127 @@ let interp_last last =
     let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s);
     raise e
 
+let update_on_end_of_segment cmd_stk id =
+  let lookup_section (_,elt) =
+    match elt with
+      | { status = ResetAtSegmentStart id' } when id = id' -> raise Exit
+      | _ -> elt.section <- false
+  in
+  try Stack.iter lookup_section cmd_stk with Exit -> ()
+
+let push_phrase cmd_stk reset_info ide_payload =
+  begin
+    match snd (reset_info.loc_ast) with
+      | VernacEndSegment (_,id) ->
+          prerr_endline "Updating on end of segment 1";
+          update_on_end_of_segment cmd_stk id
+      | _ -> ()
+  end;
+  Stack.push (ide_payload,reset_info) cmd_stk
+
+type backtrack =
+  | BacktrackToNextActiveMark
+  | BacktrackToMark of reset_mark
+  | BacktrackToModSec of Names.identifier
+  | NoBacktrack
+
+type undo_cmds = int * int * backtrack * int * identifier list
+
+let init_undo_cmds u =
+  (0,0,NoBacktrack,0,undo_info u)
+
+let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x
+let add_abort = function
+  | (n,a,b,0,l) -> (0,a+1,b,0,l)
+  | (n,a,b,p,l) -> (n,a,b,p-1,l)
+let add_qed q (n,a,b,p,l as x) =
+    if q = 0 then x else (n,a,BacktrackToNextActiveMark,p+q,l)
+let add_backtrack (n,a,b,p,l) b' = (n,a,b',p,l)
+
+let update_proofs (n,a,b,p,cur_lems) prev_lems =
+  let ncommon = List.length (Util.list_intersect cur_lems prev_lems) in
+  let openproofs = List.length cur_lems - ncommon in
+  let closedproofs = List.length prev_lems - ncommon in
+  let undos = (n,a,b,p,prev_lems) in
+  add_qed closedproofs (Util.iterate add_abort openproofs undos)
+
+let pop_command cmd_stk undos =
+  let (_,t) = Stack.top cmd_stk in
+  let (state_info,undo_info,section_info) = t.status,t.proofs,t.section in
+  let undos =
+    if section_info then
+      let undos = update_proofs undos undo_info in
+      match state_info with
+        | _ when is_vernac_tactic_command (snd t.loc_ast) ->
+            (* A tactic, active if not * below a Qed *)
+            add_undo undos
+        | ResetAtRegisteredObject mark ->
+            add_backtrack undos (BacktrackToMark mark)
+        | ResetAtSegmentStart id ->
+            add_backtrack undos (BacktrackToModSec id)
+        | _ when is_vernac_state_preserving_command (snd t.loc_ast) ->
+            undos
+        | _ ->
+            add_backtrack undos BacktrackToNextActiveMark
+            else
+              begin
+                prerr_endline "In section";
+                (* An * object * inside * a * closed * section * *)
+                add_backtrack undos BacktrackToNextActiveMark
+              end in
+  ignore (Stack.pop cmd_stk);
+  undos
+
+(* appelle Pfedit.delete_current_proof a fois
+*  * utiliser Vernacentries.vernac_abort a la place ? *)
+let apply_aborts a =
+  if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
+  try Util.repeat a Pfedit.delete_current_proof ()
+  with e -> prerr_endline "WARNING : found a closed environment"; raise e
+
+exception UndoStackExhausted
+
+(* appelle Pfedit.undo n fois
+ * utiliser vernac_undo ? *)
+let apply_tactic_undo n =
+  if n<>0 then
+    (prerr_endline ("Applying "^string_of_int n^" undos");
+     try Pfedit.undo n with _ -> raise UndoStackExhausted)
+
+
+let apply_reset = function
+  | BacktrackToMark mark -> reset_to mark
+  | BacktrackToModSec id -> reset_to_mod id
+  | NoBacktrack -> ()
+  | BacktrackToNextActiveMark -> assert false
+
+let rec apply_undos cmd_stk (n,a,b,p,l as undos) =
+  if p = 0 & b <> BacktrackToNextActiveMark then
+    begin
+      apply_aborts a;
+      try
+        apply_tactic_undo n;
+        apply_reset b
+      with UndoStackExhausted ->
+        apply_undos cmd_stk (n,0,BacktrackToNextActiveMark,p,l)
+    end
+  else
+    (* re-synchronize Coq to the current state of the stack *)
+    if Stack.is_empty cmd_stk then
+      reset_initial ()
+    else
+      begin
+        let (ide_ri,coq_ri) = Stack.top cmd_stk in
+        apply_undos cmd_stk (pop_command cmd_stk undos);
+        let reset_info = compute_reset_info coq_ri.loc_ast in
+        interp_last coq_ri.loc_ast;
+        push_phrase cmd_stk reset_info ide_ri
+      end
+
+type  tried_tactic =
+  | Interrupted
+  | Success of int (* nb of goals after *)
+  | Failed
 
 type hyp = env * evar_map *
            ((identifier * string) * constr option * constr) *
diff --git a/ide/coq.mli b/ide/coq.mli
index 3ded7b6bd..83e6ea93b 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -42,18 +42,30 @@ type undo_info = identifier list
 
 val undo_info : unit -> undo_info
 
-type reset_info = reset_status * undo_info * bool ref
+type reset_info = {
+ status : reset_status;
+ proofs : undo_info;
+ loc_ast : Util.loc * Vernacexpr.vernac_expr;
+ mutable section : bool;
+}
 
-val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
+val compute_reset_info : Util.loc * Vernacexpr.vernac_expr -> reset_info
 val reset_initial : unit -> unit
 val reset_to : reset_mark -> unit
 val reset_to_mod : identifier -> unit
 
 val init : unit -> string list
-val interp : bool -> string -> reset_info * (Util.loc * Vernacexpr.vernac_expr)
+val interp : bool -> string -> reset_info
 val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit
 val interp_and_replace : string ->
-      (reset_info * (Util.loc * Vernacexpr.vernac_expr)) * string
+      reset_info * string
+
+val push_phrase : ('a * reset_info) Stack.t -> reset_info -> 'a -> unit
+
+type undo_cmds
+val init_undo_cmds : unit -> undo_cmds
+val pop_command : ('a * reset_info) Stack.t -> undo_cmds -> undo_cmds
+val apply_undos : ('a * reset_info) Stack.t -> undo_cmds -> unit
 
 val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool
 val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool
diff --git a/ide/coqide.ml b/ide/coqide.ml
index fe71784b3..6e3d86787 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -15,10 +15,9 @@ open Coq
 open Gtk_parsing
 open Ideutils
 
-type 'a info = {start:'a;
-                stop:'a;
-                ast:Util.loc * Vernacexpr.vernac_expr;
-                reset_info:Coq.reset_info
+type ide_info = {
+  start : GText.mark;
+  stop : GText.mark;
 }
 
 
@@ -34,7 +33,7 @@ object('self)
   val message_view : GText.view
   val proof_buffer : GText.buffer
   val proof_view : GText.view
-  val cmd_stack : GText.mark info Stack.t
+  val cmd_stack : (ide_info * Coq.reset_info) Stack.t
   val mutable is_active : bool
   val mutable read_only : bool
   val mutable filename : string option
@@ -85,7 +84,7 @@ object('self)
   method send_to_coq :
     bool -> bool -> string ->
     bool -> bool -> bool ->
-    (bool*(reset_info*(Util.loc * Vernacexpr.vernac_expr))) option
+    (bool*reset_info) option
   method set_message : string -> unit
   method show_pm_goal : unit
   method show_goals : unit
@@ -104,7 +103,7 @@ type viewable_script =
      proof_view : GText.view;
      message_view : GText.view;
      analyzed_view : analyzed_views;
-     command_stack : GText.mark info Stack.t;
+     command_stack : (ide_info * Coq.reset_info) Stack.t;
     }
 
 
@@ -167,141 +166,8 @@ let on_active_view f =
 let cb = GData.clipboard Gdk.Atom.primary
 
 
-(** Coq undoing mess **
- **********************)
-
 exception Size of int
 
-let update_on_end_of_segment cmd_stk id =
-  let lookup_section = function 
-    | { reset_info = ResetAtSegmentStart id',_,_ } when id = id' -> raise Exit
-    | { reset_info = _,_,r } -> r := false
-  in
-    try Stack.iter lookup_section cmd_stk with Exit -> ()
-
-let push_phrase cmd_stk reset_info start_of_phrase_mark end_of_phrase_mark ast =
-  let x = {start = start_of_phrase_mark;
-           stop = end_of_phrase_mark;
-	   ast = ast;
-	   reset_info = reset_info
-	  } in
-  begin
-    match snd ast with
-    | VernacEndSegment (_,id) ->
-        prerr_endline "Updating on end of segment 1";
-        update_on_end_of_segment cmd_stk id
-    | _ -> ()
-  end;
-  Stack.push x cmd_stk
-
-
-let repush_phrase cmd_stk reset_info x =
-  let x = { x with reset_info = reset_info } in
-  begin
-    match snd x.ast with
-      | VernacEndSegment (_,id) ->
-          prerr_endline "Updating on end of segment 2";
-          update_on_end_of_segment cmd_stk id
-      | _ -> ()
-  end;
-  Stack.push x cmd_stk
-
-type backtrack =
-| BacktrackToNextActiveMark
-| BacktrackToMark of reset_mark
-| BacktrackToModSec of Names.identifier
-| NoBacktrack
-
-let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x
-let add_abort = function
-  | (n,a,b,0,l) -> (0,a+1,b,0,l)
-  | (n,a,b,p,l) -> (n,a,b,p-1,l)
-let add_qed q (n,a,b,p,l as x) =
-  if q = 0 then x else (n,a,BacktrackToNextActiveMark,p+q,l)
-let add_backtrack (n,a,b,p,l) b' = (n,a,b',p,l)
-
-let update_proofs (n,a,b,p,cur_lems) prev_lems =
-  let ncommon = List.length (Util.list_intersect cur_lems prev_lems) in
-  let openproofs = List.length cur_lems - ncommon in
-  let closedproofs = List.length prev_lems - ncommon in
-  let undos = (n,a,b,p,prev_lems) in
-  add_qed closedproofs (Util.iterate add_abort openproofs undos)
-
-let pop_command cmd_stk undos t =
-  let (state_info,undo_info,section_info) = t.reset_info in
-  let undos =
-    if !section_info then
-      let undos = update_proofs undos undo_info in
-      match state_info with
-      | _ when is_vernac_tactic_command (snd t.ast) ->
-	  (* A tactic, active if not below a Qed *)
-          add_undo undos
-      | ResetAtRegisteredObject mark ->
-          add_backtrack undos (BacktrackToMark mark)
-      | ResetAtSegmentStart id ->
-          add_backtrack undos (BacktrackToModSec id)
-      | _ when is_vernac_state_preserving_command (snd t.ast) ->
-	  undos
-      | _ ->
-          add_backtrack undos BacktrackToNextActiveMark
-    else
-      begin
-        prerr_endline "In section";
-      (* An object inside a closed section *)
-      add_backtrack undos BacktrackToNextActiveMark
-      end in
-  ignore (Stack.pop cmd_stk);
-  undos
-
-
-(* appelle Pfedit.delete_current_proof a fois
- * utiliser Vernacentries.vernac_abort a la place ? *)
-let apply_aborts a =
-  if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
-  try Util.repeat a Pfedit.delete_current_proof ()
-  with e -> prerr_endline "WARNING : found a closed environment"; raise e
-
-exception UndoStackExhausted
-
-(* appelle Pfedit.undo n fois
- * utiliser vernac_undo ? *)
-let apply_tactic_undo n =
-  if n<>0 then
-    (prerr_endline ("Applying "^string_of_int n^" undos");
-     try Pfedit.undo n with _ -> raise UndoStackExhausted)
-
-
-let apply_reset = function
-  | BacktrackToMark mark -> reset_to mark
-  | BacktrackToModSec id -> reset_to_mod id
-  | NoBacktrack -> ()
-  | BacktrackToNextActiveMark -> assert false
-
-let rec apply_undos cmd_stk (n,a,b,p,l as undos) =
-  if p = 0 & b <> BacktrackToNextActiveMark then
-    begin
-      apply_aborts a;
-      try
-	apply_tactic_undo n;
-	apply_reset b
-      with UndoStackExhausted ->
-	apply_undos cmd_stk (n,0,BacktrackToNextActiveMark,p,l)
-    end
-  else
-    (* re-synchronize Coq to the current state of the stack *)
-    if Stack.is_empty cmd_stk then
-      Coq.reset_initial ()
-    else
-      begin
-        let t = Stack.top cmd_stk in
-        apply_undos cmd_stk (pop_command cmd_stk undos t);
-        let reset_info = Coq.compute_reset_info (snd t.ast) in
-        interp_last t.ast;
-        repush_phrase cmd_stk reset_info t
-      end
-
-
-
 let last_cb_content = ref ""
 
 
@@ -1161,7 +1027,7 @@ object(self)
         input_view#set_editable true;
         pop_info ();
       end in
-    let mark_processed reset_info is_complete (start,stop) ast =
+    let mark_processed reset_info is_complete (start,stop) =
       let b = input_buffer in
       b#move_mark ~where:stop (`NAME "start_of_input");
       b#apply_tag
@@ -1171,13 +1037,12 @@ object(self)
              b#place_cursor stop;
              self#recenter_insert
            end;
-         let start_of_phrase_mark = `MARK (b#create_mark start) in
-         let end_of_phrase_mark = `MARK (b#create_mark stop) in
+         let ide_payload = { start = `MARK (b#create_mark start);
+                             stop = `MARK (b#create_mark stop); } in
          push_phrase
            cmd_stack
            reset_info
-           start_of_phrase_mark
-           end_of_phrase_mark ast;
+           ide_payload;
          if display_goals then self#show_goals;
          remove_tag (start,stop) in
     begin
@@ -1185,14 +1050,14 @@ object(self)
           None -> false
         | Some (loc,phrase) ->
             (match self#send_to_coq verbosely false phrase true true true with
-               | Some (is_complete,(reset_info,ast)) ->
-                   sync (mark_processed reset_info is_complete) loc ast; true
+               | Some (is_complete,reset_info) ->
+                   sync (mark_processed reset_info is_complete) loc; true
                | None -> sync remove_tag loc; false)
     end
 
   method insert_this_phrase_on_success
         show_output show_msg localize coqphrase insertphrase =
-    let mark_processed reset_info is_complete ast =
+    let mark_processed reset_info is_complete =
       let stop = self#get_start_of_input in
         if stop#starts_line then
           input_buffer#insert ~iter:stop insertphrase
@@ -1203,9 +1068,9 @@ object(self)
             (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop;
              if (self#get_insert#compare) stop <= 0 then
                input_buffer#place_cursor stop;
-             let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in
-             let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
-               push_phrase cmd_stack reset_info start_of_phrase_mark end_of_phrase_mark ast;
+             let ide_payload = { start = `MARK (input_buffer#create_mark start);
+                                 stop = `MARK (input_buffer#create_mark stop); } in
+               push_phrase cmd_stack reset_info ide_payload;
                self#show_goals;
       (*Auto insert save on success...
        try (match Coq.get_current_goals () with
@@ -1233,8 +1098,8 @@ object(self)
        | _ -> ())
        with _ -> ()*) in
       match self#send_to_coq false false coqphrase show_output show_msg localize with
-        | Some (is_complete,(reset_info,ast)) ->
-            sync (mark_processed reset_info is_complete) ast; true
+        | Some (is_complete,reset_info) ->
+            sync (mark_processed reset_info) is_complete; true
         | None ->
             sync
               (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
@@ -1279,7 +1144,7 @@ object(self)
   method reset_initial =
     sync (fun _ ->
             Stack.iter
-              (function inf ->
+              (function (inf,_) ->
                  let start = input_buffer#get_iter_at_mark inf.start in
                  let stop = input_buffer#get_iter_at_mark inf.stop in
                    input_buffer#move_mark ~where:start (`NAME "start_of_input");
@@ -1301,16 +1166,16 @@ object(self)
       if Stack.is_empty cmd_stack then
         done_smthg, undos
       else
-        let t = Stack.top cmd_stack in
-          if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then
+        let (ide_ri,_) = Stack.top cmd_stack in
+          if i#compare (input_buffer#get_iter_at_mark ide_ri.stop) < 0 then
             begin
               prerr_endline "Popped top command";
-              pop_commands true (pop_command cmd_stack undos t)
+              pop_commands true (pop_command cmd_stack undos)
             end
           else
             done_smthg, undos
     in
-    let undos = (0,0,NoBacktrack,0,undo_info()) in
+    let undos = init_undo_cmds () in
     let done_smthg, undos = pop_commands false undos in
       prerr_endline "Popped commands";
       if done_smthg then
@@ -1320,7 +1185,7 @@ object(self)
             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
+                      else input_buffer#get_iter_at_mark (fst (Stack.top cmd_stack)).stop in
                       prerr_endline "Removing (long) processed tag...";
                       input_buffer#remove_tag
                         Tags.Script.processed
@@ -1359,18 +1224,18 @@ object(self)
     if Mutex.try_lock coq_may_stop then
       (push_info "Undoing last step...";
        (try
-          let last_command = Stack.top cmd_stack in
-          let start = input_buffer#get_iter_at_mark last_command.start in
+          let (ide_ri,_) = Stack.top cmd_stack in
+          let start = input_buffer#get_iter_at_mark ide_ri.start in
           let update_input () =
             prerr_endline "Removing processed tag...";
             input_buffer#remove_tag
               Tags.Script.processed
               ~start
-              ~stop:(input_buffer#get_iter_at_mark last_command.stop);
+              ~stop:(input_buffer#get_iter_at_mark ide_ri.stop);
             input_buffer#remove_tag
               Tags.Script.unjustified
               ~start
-              ~stop:(input_buffer#get_iter_at_mark last_command.stop);
+              ~stop:(input_buffer#get_iter_at_mark ide_ri.stop);
             prerr_endline "Moving start_of_input";
             input_buffer#move_mark
               ~where:start
@@ -1380,7 +1245,7 @@ object(self)
             self#show_goals;
             self#clear_message
           in
-          let undo = pop_command cmd_stack (0,0,NoBacktrack,0,undo_info()) last_command in
+          let undo = pop_command cmd_stack (init_undo_cmds ()) in
             apply_undos cmd_stack undo;
             sync update_input ()
         with