irediced usage of matita.includes, that is now set by

[helm.git] / matita / matitacLib.ml

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 80e81c2d7386f647b10c94aed0f4016dc6ae22ab..5886c2467042b258dbf1af3b173be9244e231ee4 100644 (file)
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -69,7 +69,8 @@ let pp_times fname rc big_bang =
     let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
     let r = Unix.gettimeofday () -. big_bang in
     let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
-    let rc = if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
+    let rc,rcascii = 
+      if rc then "\e[0;32mOK\e[0m","Ok" else "\e[0;31mFAIL\e[0m","Fail" in
     let times = 
       let fmt t = 
         let seconds = int_of_float t in
@@ -82,7 +83,8 @@ let pp_times fname rc big_bang =
     in
     let s = Printf.sprintf "%-4s %s %s" rc times extra in
     print_endline s;
-    flush stdout
+    flush stdout;
+    HLog.message ("Compilation of "^Filename.basename fname^": "^rc)
 ;;
 
 let cut prefix s = 
@@ -94,7 +96,6 @@ let cut prefix s =
 ;;
 
 let rec compile fname =
-  Helm_registry.set_string "matita.filename" fname;
   (* initialization, MOVE OUTSIDE *)
   let matita_debug = Helm_registry.get_bool "matita.debug" in
   let clean_baseuri = not (Helm_registry.get_bool "matita.preserve") in    
@@ -102,7 +103,7 @@ let rec compile fname =
     Helm_registry.get_list Helm_registry.string "matita.includes" 
   in
   (* sanity checks *)
-  let root,baseuri,fname = Librarian.baseuri_of_script ~include_paths fname in
+  let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in
   let moo_fname = 
    LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true
   in
@@ -221,3 +222,32 @@ let rec compile fname =
        clean_exit baseuri false
 ;;
 
+module F = 
+  struct 
+    type source_object = string
+    type target_object = string
+    let string_of_source_object s = s;;
+    let string_of_target_object s = s;;
+
+    let target_of mafile = 
+      let _,baseuri,_,_ = Librarian.baseuri_of_script mafile in
+      LibraryMisc.obj_file_of_baseuri 
+        ~must_exist:false ~baseuri ~writable:true 
+    ;;
+
+    let mtime_of_source_object s =
+      try Some (Unix.stat s).Unix.st_mtime
+      with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> 
+        raise (Failure ("Unable to stat a source file: " ^ s)) 
+    ;;
+
+    let mtime_of_target_object s =
+      try Some (Unix.stat s).Unix.st_mtime
+      with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
+    ;;
+
+    let build = compile;;
+  end 
+
+module Make = Make.Make(F) 
+