Bug fixed: we used to use iterators on a text that was modified, making

Gtk raise non-critical erros.

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index ad4592a67ec028c545afb948c88e5b51a949464a..4425d10218521600380b721216d8b98569e636b5 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -594,34 +594,36 @@ 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 
+    let getoffset () = (buffer#get_iter_at_mark (`MARK locked_mark))#offset in 
     match pos with
     | `Top -> self#goto_top; self#notify
     | `Bottom ->
         (try 
           let rec dowhile pos =
             self#_advance ();
-            if pos#compare (getpos ()) < 0 then
-              dowhile (getpos ())
+            let newpos = getoffset () in
+            if pos - newpos < 0 then
+              dowhile newpos
           in
-          dowhile (getpos ());
+          dowhile (getoffset ());
           self#notify 
         with 
         | Margin -> self#notify
         | 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 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 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 
+            if (locked_offset ()) - cursor_offset () < 0 &&
+               oldpos - (getoffset ()) < 0 
             then
-              aux (getpos ())
+              aux (getoffset ())
           in
-          aux (getpos ())
+          aux (getoffset ())
         in
         let rec back_until_cursor len = (* go backward until locked < cursor *)
          function