all interface is locked during advance/retract

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index d145eec2025dd6f4b247aa17a46d72ecfa647914..b077021e3caf21227e56241086ad32bca5162166 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -497,11 +497,11 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
     set_star self#ppFilename false
 
   method goto (pos: [`Top | `Bottom | `Cursor]) () =
+    let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in 
     match pos with
     | `Top -> self#goto_top; self#notify
     | `Bottom ->
         (try 
-          let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in 
           let rec dowhile pos =
             self#_advance ();
             if pos#compare (getpos ()) < 0 then
@@ -515,10 +515,15 @@ 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 rec forward_until_cursor () = (* go forward until locked > cursor *)
-          self#_advance ();
-          if (locked_iter ())#compare (cursor_iter ()) < 0 then
-            forward_until_cursor ()
+        let forward_until_cursor () = (* go forward until locked > cursor *)
+          let rec aux oldpos =
+            self#_advance ();
+            if (locked_iter ())#compare (cursor_iter ()) < 0 &&
+               oldpos#compare (getpos ()) < 0 
+            then
+              aux (getpos ())
+          in
+          aux (getpos ())
         in
         let rec back_until_cursor () = (* go backward until locked < cursor *)
           self#_retract ();