X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FmatitaEngine.ml;fp=matitaB%2Fmatita%2FmatitaEngine.ml;h=aa271b2a1ca948b69ae67c3c008fd871e479fb59;hb=d8ae533d041cb600993ab2957111c105b6ded21d;hp=9c86679bc420789579639adda15aa29d6676e615;hpb=13935d33cc0899b9555648a4d49586e17274c748;p=helm.git

diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index 9c86679bc..aa271b2a1 100644
--- a/matitaB/matita/matitaEngine.ml
+++ b/matitaB/matita/matitaEngine.ml
@@ -140,7 +140,7 @@ let rec get_ast status ~compiling ~asserted ~include_paths strm =
        let already_included = NCicLibrary.get_transitively_included status in
        let asserted,_ =
         assert_ng ~already_included ~compiling ~asserted ~include_paths
-         mafilename
+         ?uid:status#user mafilename
        in
         asserted,cmd
    | cmd -> asserted,cmd
@@ -168,7 +168,7 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status
  in
   loop asserted status
 
-and compile ~compiling ~asserted ~include_paths ~outch fname =
+and compile ~compiling ~asserted ~include_paths ~outch ?uid fname =
   if List.mem fname compiling then raise (CircularDependency fname);
   let compiling = fname::compiling in
   let matita_debug = Helm_registry.get_bool "matita.debug" in
@@ -178,7 +178,7 @@ and compile ~compiling ~asserted ~include_paths ~outch fname =
   activate_extraction baseuri fname ;
   (* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
   (* FIXME: currently hardcoded to single user mode *)
-  let status = new status None baseuri in
+  let status = new status uid baseuri in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times () 
@@ -263,6 +263,9 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid
    let baseuri = NUri.uri_of_string baseuri in
    let ngtime_of baseuri =
     let ngpath = NCicLibrary.ng_path_of_baseuri uid baseuri in
+    let uid = match uid with Some u -> "Some " ^ u | _ -> "None" in
+    prerr_endline ("uid = " ^ uid);
+    prerr_endline ("ngpath = " ^ ngpath);
     try
      Some (Unix.stat ngpath).Unix.st_mtime
     with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
@@ -280,7 +283,7 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid
           (fun (asserted,b) mapath ->
             let asserted,b1 =
               assert_ng ~already_included ~compiling ~asserted ~include_paths
-               mapath
+                ?uid mapath
             in
              asserted, b || b1
               || let _,baseuri,_,_ =
@@ -294,6 +297,7 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid
          asserted, children_bad || matime > ngtime
      | None -> asserted,true
    in
+    prerr_endline ("asserted = " ^ (String.concat "," asserted));
     if not to_be_compiled then fullmapath::asserted,false
     else
      if List.mem baseuri already_included then
@@ -305,7 +309,8 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid
         | None -> open_out (fullmapath ^ ".mad"), true
         | Some c -> c, false
       in
-      let asserted = compile ~compiling ~asserted ~include_paths ~outch fullmapath in
+      prerr_endline ("compiling " ^ fullmapath);
+      let asserted = compile ~compiling ~asserted ~include_paths ~outch ?uid fullmapath in
        if is_file_ch then close_out outch;
        fullmapath::asserted,true
   end