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).

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 7e4dcb9fc04e4200a8c00e15a77c02af7e617a37..86775f2923dcb041b606c8d30a303d912c7115f0 100644 (file)
--- 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