Turbo-undo implemented! It jumps directly to the final position after the undo.

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index e31dd7a1540e5642fde6d525bad6f4d1aac10a3f..aae0e93d78a857fcbf14587eaa736c59f9bd526a 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -464,14 +464,12 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
       end;
     self#moveMark (String.length new_text)
 
-  method private _retract () =
-    match statements, history with
-    | last_statement :: _, cur_status :: prev_status :: _ ->
-        MatitaSync.time_travel ~present:cur_status ~past:prev_status;
-        statements <- List.tl statements;
-        history <- List.tl history;
-        self#moveMark (- (String.length last_statement));
-    | _ -> raise Margin
+  method private _retract offset status new_statements new_history =
+   let cur_status = match history with s::_ -> s | [] -> assert false in
+    MatitaSync.time_travel ~present:cur_status ~past:status;
+    statements <- new_statements;
+    history <- new_history;
+    self#moveMark (- offset)
 
   method advance ?statement () =
     try
@@ -483,8 +481,15 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
 
   method retract () =
     try
-      self#_retract ();
-      self#notify
+      let cmp,new_statements,new_history,status =
+       match statements,history with
+          stat::statements, _::(status::_ as history) ->
+           String.length stat, statements, history, status
+       | [],[_] -> raise Margin
+       | _,_ -> assert false
+      in
+       self#_retract cmp status new_statements new_history;
+       self#notify
     with 
     | Margin -> self#notify
     | exc -> self#notify; raise exc
@@ -599,6 +604,7 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     | `Cursor ->
         let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
         let cursor_iter () = buffer#get_iter_at_mark `INSERT in
+        let cmp = (locked_iter ())#offset - (cursor_iter ())#offset in
         let forward_until_cursor () = (* go forward until locked > cursor *)
           let rec aux oldpos =
             self#_advance ();
@@ -609,17 +615,19 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
           in
           aux (getpos ())
         in
-        let rec back_until_cursor () = (* go backward until locked < cursor *)
-          self#_retract ();
-          if (locked_iter ())#compare (cursor_iter ()) > 0 then
-            back_until_cursor ()
+        let rec back_until_cursor len = (* go backward until locked < cursor *)
+         function
+            statements, (status::_ as history) when len <= 0 ->
+             self#_retract (cmp - len) status statements history
+          | statement::tl1, _::tl2 ->
+             back_until_cursor (len - String.length statement) (tl1,tl2)
+          | _,_ -> assert false
         in
-        let cmp = (locked_iter ())#compare (cursor_iter ()) in
         (try
           if cmp < 0 then       (* locked < cursor *)
             (forward_until_cursor (); self#notify)
           else if cmp > 0 then  (* locked > cursor *)
-            (back_until_cursor (); self#notify)
+            (back_until_cursor cmp (statements,history); self#notify)
           else                  (* cursor = locked *)
               ()
         with