From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 13 Jul 2005 15:52:10 +0000 (+0000)
Subject: all interface is locked during advance/retract
X-Git-Tag: pre_notation~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=904ecbd458b20b47d250889459f9aa9ebd26d04d;p=helm.git

all interface is locked during advance/retract
---

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 4f77603ad..1f035a0fa 100644
--- 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 b54dbb777..652c720b9 100644
--- 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 d145eec20..b077021e3 100644
--- 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 ();