From 4920c541a0fa7a5b8eedbe03533fda63be7f4079 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 18 Jul 2005 15:40:57 +0000 Subject: [PATCH] Turbo-undo implemented! It jumps directly to the final position after the undo. --- helm/matita/matitaScript.ml | 40 ++++++++++++++++++++++--------------- 1 file changed, 24 insertions(+), 16 deletions(-) diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index e31dd7a15..aae0e93d7 100644 --- 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 -- 2.39.2