ready for 0.1.1 release

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

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 2b3a4b394cbaf6b3e6215c39c214526c7853123e..6e0d5660cd62148b2cade6a99410495da25fad48 100644 (file)
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -125,17 +125,16 @@ let rebuild_makefile development =
   let rm = BuildTimeConf.runtime_base_dir ^ "/matitaclean" ^ am_i_opt () in
   let mm = BuildTimeConf.runtime_base_dir ^ "/matitadep" ^ am_i_opt () in
   let df = pool () ^ development.name ^ "/depend" in
-  let dfs = pool () ^ development.name ^ "/depend.short" in
   let template = Pcre.replace ~pat:"@ROOT@" ~templ:development.root template in
   let template = Pcre.replace ~pat:"@CC@" ~templ:cc template in
   let template = Pcre.replace ~pat:"@DEP@" ~templ:mm template in
   let template = Pcre.replace ~pat:"@DEPFILE@" ~templ:df template in
-  let template = Pcre.replace ~pat:"@DEPFILESHORT@" ~templ:dfs template in
   let template = Pcre.replace ~pat:"@CLEAN@" ~templ:rm template in
   MatitaMisc.output_file template makefilepath
   
 (* creates a new development if possible *)
 let initialize_development name dir =
+  let name = Pcre.replace ~pat:" " ~templ:"_" name in 
   let dev = {name = name ; root = dir} in
   match development_for_dir dir with
   | Some d ->
@@ -156,7 +155,10 @@ let make chdir args =
   let old = Unix.getcwd () in
   try
     Unix.chdir chdir;
-    let rc = Unix.system (String.concat " " ("make"::args)) in
+    let rc = 
+      Unix.system 
+        (String.concat " " ("make"::(List.map Filename.quote args)))
+    in
     Unix.chdir old;
     match rc with
     | Unix.WEXITED 0 -> true
@@ -175,8 +177,6 @@ let call_make development target make =
 let build_development ?(target="all") development =
   call_make development target make
 
-exception CHILD_DEAD
-  
 (* not really good vt100 *)
 let vt100 s =
   let rex = Pcre.regexp "\e\\[[0-9;]+m" in
@@ -213,10 +213,8 @@ let mk_maker refresh_cb =
     let out_r,out_w = Unix.pipe () in
     let err_r,err_w = Unix.pipe () in
     let pid = ref ~-1 in
+    ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore));
     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;
@@ -225,6 +223,10 @@ let mk_maker refresh_cb =
       let rec aux = function 
         | f::tl ->
             let len = Unix.read f buf 0 1024 in
+            if len = 0 then 
+              raise 
+                (Unix.Unix_error 
+                  (Unix.EPIPE,"read","len = 0 (matita internal)"));
             vt100 (String.sub buf 0 len);
             aux tl
         | _ -> ()
@@ -235,14 +237,9 @@ let mk_maker refresh_cb =
         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)
-  
+    with 
+    | Unix.Unix_error (_,"read",_)
+    | Unix.Unix_error (_,"select",_) -> true)
 
 let build_development_in_bg ?(target="all") refresh_cb development =
   call_make development target (mk_maker refresh_cb)
@@ -254,7 +251,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 
@@ -274,7 +271,6 @@ let destroy_development development =
     unlink (makefile_for_development development);
     unlink (pool () ^ development.name ^ rootfile);
     unlink (pool () ^ development.name ^ "/depend");
-    unlink (pool () ^ development.name ^ "/depend.short");
     rmdir (pool () ^ development.name);
     developments := 
       List.filter (fun d -> d.name <> development.name) !developments
@@ -285,6 +281,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