all interface is locked during advance/retract

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

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;