all interface is locked during advance/retract

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 4f77603adc88fbdc86d000114e30a39f88af6d39..1f035a0faff843113ee9a5badf7e44ae20eb6f85 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -1773,7 +1773,7 @@ Copyright (C) 2005,
                          <property name="spacing">0</property>
 
                          <child>
-                           <widget class="GtkToolbar" id="toolbar13">
+                           <widget class="GtkToolbar" id="buttonsToolbar">
                              <property name="visible">True</property>
                              <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
                              <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index b54dbb777f2e57f7e898d5510f7dcf7b0232ca03..652c720b96dadf7c0b502d35ca5747777c081618 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -339,11 +339,29 @@ class gui () =
         source_buffer#place_cursor
           (source_buffer#get_iter_at_mark (`NAME "locked"))
       in
+      let lock_world _ =
+        main#buttonsToolbar#misc#set_sensitive false;
+        source_view#set_editable false
+      in
+      let unlock_world _ =
+        main#buttonsToolbar#misc#set_sensitive true;
+        source_view#set_editable true
+      in
       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
       let retract _ = (MatitaScript.instance ())#retract (); cursor () in
       let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
       let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
       let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
+      let locker f = 
+        fun () -> 
+          lock_world ();
+          try f ();unlock_world () with exc -> unlock_world (); raise exc
+      in
+      let advance = locker advance in
+      let retract = locker retract in
+      let top = locker top in
+      let bottom = locker bottom in
+      let jump = locker jump in
       let connect_key sym f =
         connect_key self#main#mainWinEventBox#event
           ~modifiers:[`CONTROL] ~stop:true sym f;

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 ();