Bug fixed: clicking on a new position while advancing/retracting now

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index e0e4227dd1f5709d921b4bd57f3bf8b0df6594dd..c2b9a7e93615d6120784a0f1dfdf34bf30fdfe0b 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -611,12 +611,12 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
         | exc -> self#notify; raise exc)
     | `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 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 ();
-            if (locked_iter ())#compare (cursor_iter ()) < 0 &&
+            if (locked_iter ())#compare cursor_iter < 0 &&
                oldpos#compare (getpos ()) < 0 
             then
               aux (getpos ())