Regression fixed: goto used to stop (again!) to the new cursor position when

[helm.git] / helm / matita / matitaScript.ml

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