compilation of needed modules now outputs to the log window

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

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 512da157ae5cbdedfbe56b46b36a400699d31aa5..2b3a4b394cbaf6b3e6215c39c214526c7853123e 100644 (file)
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -166,17 +166,93 @@ let make chdir args =
     logger `Warning ("Unix Error: " ^ cmd ^ ": " ^ err);
     false
       
-let call_make development target =
+let call_make development target make =
   rebuild_makefile development;
   let makefile = makefile_for_development development in
   make development.root 
     ["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target]
       
 let build_development ?(target="all") development =
-  call_make development target
+  call_make development target make
+
+exception CHILD_DEAD
+  
+(* not really good vt100 *)
+let vt100 s =
+  let rex = Pcre.regexp "\e\\[[0-9;]+m" in
+  let rex_i = Pcre.regexp "^Info" in
+  let rex_w = Pcre.regexp "^Warning" in
+  let rex_e = Pcre.regexp "^Error" in
+  let rex_d = Pcre.regexp "^Debug" in
+  let rex_noendline = Pcre.regexp "\\n" in
+  let s = Pcre.replace ~rex:rex_noendline s in
+  let len = String.length s in
+  let tokens = Pcre.split ~rex s in
+  let logger = ref MatitaLog.message in
+  let rec aux = 
+    function
+    | [] -> ()
+    | s::tl ->
+        (if Pcre.pmatch ~rex:rex_i s then
+          logger := MatitaLog.message
+        else if Pcre.pmatch ~rex:rex_w s then
+          logger := MatitaLog.warn
+        else if Pcre.pmatch ~rex:rex_e s then
+          logger := MatitaLog.error
+        else if Pcre.pmatch ~rex:rex_d s then
+          logger := MatitaLog.debug
+        else 
+          !logger s);
+        aux tl
+  in
+  aux tokens
   
+
+let mk_maker refresh_cb =
+  (fun chdir args ->
+    let out_r,out_w = Unix.pipe () in
+    let err_r,err_w = Unix.pipe () in
+    let pid = ref ~-1 in
+    try 
+      let _ = 
+        Sys.signal Sys.sigchld (Sys.Signal_handle (fun _ -> raise CHILD_DEAD))
+      in
+      let argv = Array.of_list ("make"::args) in
+      pid := Unix.create_process "make" argv Unix.stdin out_w err_w;
+      Unix.close out_w;
+      Unix.close err_w;
+      let buf = String.create 1024 in
+      let rec aux = function 
+        | f::tl ->
+            let len = Unix.read f buf 0 1024 in
+            vt100 (String.sub buf 0 len);
+            aux tl
+        | _ -> ()
+      in
+      while true do
+        let r,_,_ = Unix.select [out_r; err_r] [] [] (-. 1.) in
+        aux r;
+        refresh_cb ()
+      done;
+      true
+    with CHILD_DEAD -> 
+      let _, status = Unix.waitpid [] !pid in
+      match status with
+      | Unix.WEXITED 0 -> 
+          ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore));
+          true
+      | _ -> false)
+  
+
+let build_development_in_bg ?(target="all") refresh_cb development =
+  call_make development target (mk_maker refresh_cb)
+;;
+
 let clean_development development =
-  call_make development "clean"
+  call_make development "clean" make
+
+let clean_development_in_bg refresh_cb development =
+  call_make development "clean" (mk_maker refresh_cb)
 
 let destroy_development development =
   let delete_development development =