X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitamakeLib.ml;h=8eba26fb02cbb8556187d89844c49f4a53a59022;hb=ef465722a7f3314832fa4ef2d0265288ee74c87b;hp=55029914ec12e1089f11c7af245b5fe0277ff29c;hpb=b10f12ffbe85d3926e4de4e688bc6e41f5a6f2c0;p=helm.git

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 55029914e..8eba26fb0 100644
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -23,12 +23,14 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 let logger = fun mark -> 
   match mark with 
-  | `Error -> MatitaLog.error
-  | `Warning -> MatitaLog.warn
-  | `Debug -> MatitaLog.debug
-  | `Message -> MatitaLog.message
+  | `Error -> HLog.error
+  | `Warning -> HLog.warn
+  | `Debug -> HLog.debug
+  | `Message -> HLog.message
 ;;
 
 type development = 
@@ -55,7 +57,7 @@ let ls_dir dir =
 
 let initialize () = 
   (* create a base env if none *)
-  MatitaMisc.mkdir (pool ());
+  HExtlib.mkdir (pool ());
   (* load developments *)
   match ls_dir (pool ()) with
   | None -> logger `Error ("Unable to list directory " ^ pool ()) 
@@ -64,7 +66,7 @@ let initialize () =
         (fun name -> 
           let root = 
             try 
-              Some (MatitaMisc.input_file (pool () ^ name ^ rootfile))
+              Some (HExtlib.input_file (pool () ^ name ^ rootfile))
             with Unix.Unix_error _ -> 
               logger `Warning ("Malformed development " ^ name);
               None
@@ -106,8 +108,8 @@ let development_for_name name =
 (* dumps the deveopment to disk *)
 let dump_development devel =
   let devel_dir = pool () ^ devel.name in 
-  MatitaMisc.mkdir devel_dir;
-  MatitaMisc.output_file devel.root (devel_dir ^ rootfile);
+  HExtlib.mkdir devel_dir;
+  HExtlib.output_file ~filename:(devel_dir ^ rootfile) ~text:devel.root
 ;;
 
 let list_known_developments () = 
@@ -119,7 +121,7 @@ let am_i_opt () =
 let rebuild_makefile development = 
   let makefilepath = makefile_for_development development in
   let template = 
-    MatitaMisc.input_file BuildTimeConf.matitamake_makefile_template 
+    HExtlib.input_file BuildTimeConf.matitamake_makefile_template 
   in
   let cc = BuildTimeConf.runtime_base_dir ^ "/matitac" ^ am_i_opt () in
   let rm = BuildTimeConf.runtime_base_dir ^ "/matitaclean" ^ am_i_opt () in
@@ -130,10 +132,11 @@ let rebuild_makefile development =
   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:"@CLEAN@" ~templ:rm template in
-  MatitaMisc.output_file template makefilepath
+  HExtlib.output_file ~filename:makefilepath ~text:template
   
 (* 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 ->
@@ -154,7 +157,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
@@ -167,8 +173,13 @@ let make chdir args =
 let call_make development target make =
   rebuild_makefile development;
   let makefile = makefile_for_development development in
+  let nodb =
+    Helm_registry.get_opt_default Helm_registry.bool ~default:false "db.nodb"
+  in
+  let flags = if nodb then ["NODB=true"] else [] in
   make development.root 
-    ["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target]
+    (["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target]
+    @ flags)
       
 let build_development ?(target="all") development =
   call_make development target make
@@ -182,21 +193,20 @@ let vt100 s =
   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 logger = ref HLog.message in
   let rec aux = 
     function
     | [] -> ()
     | s::tl ->
         (if Pcre.pmatch ~rex:rex_i s then
-          logger := MatitaLog.message
+          logger := HLog.message
         else if Pcre.pmatch ~rex:rex_w s then
-          logger := MatitaLog.warn
+          logger := HLog.warn
         else if Pcre.pmatch ~rex:rex_e s then
-          logger := MatitaLog.error
+          logger := HLog.error
         else if Pcre.pmatch ~rex:rex_d s then
-          logger := MatitaLog.debug
+          logger := HLog.debug
         else 
           !logger s);
         aux tl