From 6ba0b48cb9e6a399d4519d40bc65a658d99a3c13 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 21 Jul 2005 16:32:20 +0000
Subject: [PATCH] Regression fixed: goto used to stop (again!) to the new
 cursor position when the user clicks somewhere. The source of the regression
 was the difficulty of remembering the position of the marks while the text is
 modified (by automatic insertion of aliases). Solved by using ad-hoc
 temporary marks in place of iterators (first version tried) and offsets (most
 recent version tried).

---
 helm/matita/matitaScript.ml | 78 ++++++++++++++++++++++++-------------
 1 file changed, 51 insertions(+), 27 deletions(-)

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 7e4dcb9fc..86775f292 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -594,55 +594,79 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     set_star self#ppFilename false
 
   method goto (pos: [`Top | `Bottom | `Cursor]) () =
-    let getoffset () = (buffer#get_iter_at_mark (`MARK locked_mark))#offset in 
+    let old_locked_mark =
+     `MARK
+       (buffer#create_mark ~name:"old_locked_mark"
+         ~left_gravity:true (buffer#get_iter_at_mark (`MARK locked_mark))) in
+    let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in 
+    let getoldpos _ = buffer#get_iter_at_mark old_locked_mark in 
+    let dispose_old_locked_mark () = buffer#delete_mark old_locked_mark in
     match pos with
-    | `Top -> self#goto_top; self#notify
+    | `Top -> dispose_old_locked_mark (); self#goto_top; self#notify
     | `Bottom ->
         (try 
-          let rec dowhile pos =
+          let rec dowhile () =
             self#_advance ();
-            let newpos = getoffset () in
-            if pos - newpos < 0 then
-              dowhile newpos
+            let newpos = getpos () in
+            if (getoldpos ())#compare newpos < 0 then
+              begin
+                buffer#move_mark old_locked_mark newpos;
+                dowhile ()
+              end
           in
-          dowhile (getoffset ());
+          dowhile ();
+          dispose_old_locked_mark ();
           self#notify 
         with 
-        | Margin -> self#notify
-        | exc -> self#notify; raise exc)
+        | Margin -> dispose_old_locked_mark (); self#notify
+        | exc -> dispose_old_locked_mark (); self#notify; raise exc)
     | `Cursor ->
-        let locked_offset () =
-         (buffer#get_iter_at_mark (`NAME "locked"))#offset in
-        let cursor_offset () = (buffer#get_iter_at_mark `INSERT)#offset in
-        let cmp = (locked_offset ()) - cursor_offset () in
+        let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
+        let cursor_iter () = buffer#get_iter_at_mark `INSERT in
+        let remember =
+         `MARK
+           (buffer#create_mark ~name:"initial_insert"
+             ~left_gravity:true (cursor_iter ())) in
+        let dispose_remember () = buffer#delete_mark remember in
+        let remember_iter () =
+         buffer#get_iter_at_mark (`NAME "initial_insert") in
+        let cmp () = (locked_iter ())#offset - (remember_iter ())#offset in
+        let icmp = cmp () in
         let forward_until_cursor () = (* go forward until locked > cursor *)
-          let rec aux oldpos =
+          let rec aux () =
             self#_advance ();
-            if (locked_offset ()) - cursor_offset () < 0 &&
-               oldpos - (getoffset ()) < 0 
+            if cmp () < 0 && (getoldpos ())#compare (getpos ()) < 0 
             then
-              aux (getoffset ())
+             begin
+              buffer#move_mark old_locked_mark (getpos ());
+              aux ()
+             end
           in
-          aux (getoffset ())
+          aux ()
         in
         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
+             self#_retract (icmp - len) status statements history
           | statement::tl1, _::tl2 ->
              back_until_cursor (len - String.length statement) (tl1,tl2)
           | _,_ -> assert false
         in
         (try
-          if cmp < 0 then       (* locked < cursor *)
-            (forward_until_cursor (); self#notify)
-          else if cmp > 0 then  (* locked > cursor *)
-            (back_until_cursor cmp (statements,history); self#notify)
-          else                  (* cursor = locked *)
-              ()
+          begin
+           if icmp < 0 then       (* locked < cursor *)
+             (forward_until_cursor (); self#notify)
+           else if icmp > 0 then  (* locked > cursor *)
+             (back_until_cursor icmp (statements,history); self#notify)
+           else                  (* cursor = locked *)
+               ()
+          end ;
+          dispose_remember ();
+          dispose_old_locked_mark ();
         with 
-        | Margin -> self#notify
-        | exc -> self#notify; raise exc)
+        | Margin -> dispose_remember (); dispose_old_locked_mark (); self#notify
+        | exc -> dispose_remember (); dispose_old_locked_mark ();
+                 self#notify; raise exc)
               
   method onGoingProof () =
     match self#status.proof_status with
-- 
2.39.2