compilation of needed modules now outputs to the log window

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index efe629ac1903d8954781314b1109bdefbf34d8f2..1d433f848a2f988dd42cde1c313c5048abbc15ad 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -225,16 +225,21 @@ class gui () =
           | None -> ()
           | Some d -> MatitamakeLib.destroy_development d);
           refresh_devels_win ());
+      let refresh () = 
+        while Glib.Main.pending () do 
+          ignore(Glib.Main.iteration false); 
+        done
+      in
       connect_button develList#buildButton 
         (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.build_development d));
+          | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d));
       connect_button develList#cleanButton 
         (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.clean_development d));
+          | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete