Multi-user matita: changed the status object to include a ``user'' method

[helm.git] / matitaB / matita / matitaEngine.ml

diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index 437121b73f9aed171ba0184763b2d810ba1a7773..9c86679bc420789579639adda15aa29d6676e615 100644 (file)
--- a/matitaB/matita/matitaEngine.ml
+++ b/matitaB/matita/matitaEngine.ml
@@ -29,10 +29,10 @@ module G = GrafiteAst
 open GrafiteTypes
 open Printf
 
-class status baseuri =
+class status uid baseuri =
  object
-  inherit GrafiteTypes.status baseuri
-  inherit ApplyTransformation.status
+  inherit GrafiteTypes.status uid baseuri
+  inherit ApplyTransformation.status uid
  end
 
 exception TryingToAdd of string Lazy.t
@@ -177,7 +177,8 @@ and compile ~compiling ~asserted ~include_paths ~outch fname =
   if Http_getter_storage.is_read_only baseuri then assert false;
   activate_extraction baseuri fname ;
   (* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
-  let status = new status baseuri in
+  (* FIXME: currently hardcoded to single user mode *)
+  let status = new status None baseuri in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times () 
@@ -254,14 +255,14 @@ and compile ~compiling ~asserted ~include_paths ~outch fname =
       pp_times fname false big_bang big_bang_u big_bang_s;
       clean_exit baseuri exn
 
-and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch mapath =
+and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid mapath =
  let _,baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
  if List.mem fullmapath asserted then asserted,false
  else
   begin
    let baseuri = NUri.uri_of_string baseuri in
    let ngtime_of baseuri =
-    let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
+    let ngpath = NCicLibrary.ng_path_of_baseuri uid baseuri in
     try
      Some (Unix.stat ngpath).Unix.st_mtime
     with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
@@ -273,7 +274,7 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch mapat
    let asserted,to_be_compiled =
     match ngtime with
        Some ngtime ->
-        let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
+        let preamble = GrafiteTypes.Serializer.dependencies_of uid baseuri in
         let asserted,children_bad =
          List.fold_left
           (fun (asserted,b) mapath ->