better handling of backgroud compiler process

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index eb75ac11042da2148a198472aebeaa33047583db..f884bee2eba41145b2b9f7b33182701f6eba6c1f 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -325,6 +325,20 @@ class gui () =
       ignore(self#main#findReplMenuItem#connect#activate
         ~callback:show_find_Repl);
       ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
+        (* interface lockers *)
+      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 locker f = 
+        fun () -> 
+          lock_world ();
+          try f ();unlock_world () with exc -> unlock_world (); raise exc
+      in
         (* developments win *)
       let model = 
         new MatitaGtkMisc.multiStringListModel 
@@ -360,12 +374,20 @@ class gui () =
         (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d));
+          | Some d -> 
+              let build = locker 
+                (fun () -> MatitamakeLib.build_development_in_bg refresh d)
+              in
+              ignore(build ()));
       connect_button develList#cleanButton 
         (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
+          | Some d -> 
+              let clean = locker 
+                (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
+              in
+              ignore(clean ()));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete 
@@ -575,24 +597,11 @@ 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