building/cleaning a devel now makes buttons insensitive

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 9d90662144a6cebfe119c919b3b9e9a4b37bc15b..a99cb2db11ccbe96b57a1267d2b340f585981571 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -3451,7 +3451,7 @@
       </child>
 
       <child>
-       <widget class="GtkHBox" id="hbox22">
+       <widget class="GtkHBox" id="buttonsHbox">
          <property name="border_width">3</property>
          <property name="visible">True</property>
          <property name="homogeneous">False</property>

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index d21241a8dd4bc3c84afcb958b440454221a47196..f83e01913d7fb1c26281e4ef5a60492e39301b67 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -347,10 +347,12 @@ class gui () =
         (* interface lockers *)
       let lock_world _ =
         main#buttonsToolbar#misc#set_sensitive false;
+        develList#buttonsHbox#misc#set_sensitive false;
         source_view#set_editable false
       in
       let unlock_world _ =
         main#buttonsToolbar#misc#set_sensitive true;
+        develList#buttonsHbox#misc#set_sensitive true;
         source_view#set_editable true
       in
       let locker f = 
@@ -374,39 +376,39 @@ class gui () =
         | [[name;_]] -> MatitamakeLib.development_for_name name
         | _ -> assert false 
       in
+      let refresh () = 
+        while Glib.Main.pending () do 
+          ignore(Glib.Main.iteration false); 
+        done
+      in
       connect_button develList#newButton
         (fun () -> 
           next_devel_must_contain <- None;
           newDevel#toplevel#misc#show());
       connect_button develList#deleteButton
-        (fun () -> 
+        (locker (fun () -> 
           (match get_devel_selected () with
           | None -> ()
-          | Some d -> MatitamakeLib.destroy_development d);
-          refresh_devels_win ());
-      let refresh () = 
-        while Glib.Main.pending () do 
-          ignore(Glib.Main.iteration false); 
-        done
-      in
+          | Some d -> MatitamakeLib.destroy_development_in_bg refresh d);
+          refresh_devels_win ()));
       connect_button develList#buildButton 
-        (fun () -> 
+        (locker (fun () -> 
           match get_devel_selected () with
           | None -> ()
           | Some d -> 
               let build = locker 
                 (fun () -> MatitamakeLib.build_development_in_bg refresh d)
               in
-              ignore(build ()));
+              ignore(build ())));
       connect_button develList#cleanButton 
-        (fun () -> 
+        (locker (fun () -> 
           match get_devel_selected () with
           | None -> ()
           | Some d -> 
               let clean = locker 
                 (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
               in
-              ignore(clean ()));
+              ignore(clean ())));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete 

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 48d6696281248cda435447c4f59a55e38936668c..55029914ec12e1089f11c7af245b5fe0277ff29c 100644 (file)
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -247,7 +247,7 @@ let clean_development development =
 let clean_development_in_bg refresh_cb development =
   call_make development "clean" (mk_maker refresh_cb)
 
-let destroy_development development =
+let destroy_development_aux development clean_development =
   let delete_development development = 
     let unlink file =
       try 
@@ -277,6 +277,12 @@ let destroy_development development =
       logger `Warning "This may cause garbage."
     end;
   delete_development development 
+ 
+let destroy_development development = 
+  destroy_development_aux development clean_development
+
+let destroy_development_in_bg refresh development = 
+  destroy_development_aux development (clean_development_in_bg refresh) 
   
 let root_for_development development = development.root
 let name_for_development development = development.name

diff --git a/helm/matita/matitamakeLib.mli b/helm/matita/matitamakeLib.mli
index 1dd697e5dcd9b56397c0f84425b5c9bf15ad6945..4aaab47b13f4eaf8c9ea26ad14d2f0a4ad6a4b28 100644 (file)
--- a/helm/matita/matitamakeLib.mli
+++ b/helm/matita/matitamakeLib.mli
@@ -44,6 +44,7 @@ val development_for_name: string -> development option
 val list_known_developments: unit -> (string * string ) list
 (* cleans the development, forgetting about it *)
 val destroy_development: development -> unit
+val destroy_development_in_bg: (unit -> unit) -> development -> unit
 (* initiale internal data structures *)
 val initialize : unit -> unit
 (* gives back the root *)