compilation of needed modules now outputs to the log window

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index f1a0e6429622490e4973fd1aa218ff284e33a3cc..e31dd7a1540e5642fde6d525bad6f4d1aac10a3f 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -151,7 +151,10 @@ let eval_with_engine guistuff status user_goal parsed_text st =
       let compile_needed_and_go_on d =
         let root = MatitamakeLib.root_for_development d in
         let target = root ^ "/" ^ what in
-        if not(MatitamakeLib.build_development ~target d) then
+        let refresh_cb () = 
+          while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
+        in
+        if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then
           raise exc
         else
           eval_with_engine guistuff status user_goal parsed_text st