(no commit message)

[helm.git] / matitaB / components / ng_library / nCicLibrary.ml

diff --git a/matitaB/components/ng_library/nCicLibrary.ml b/matitaB/components/ng_library/nCicLibrary.ml
index 201b5ac082b8a425726a4859db1c6c2f371f9a62..a7e35f42796500ab47b434d2b7980b09a90bf04f 100644 (file)
--- a/matitaB/components/ng_library/nCicLibrary.ml
+++ b/matitaB/components/ng_library/nCicLibrary.ml
@@ -16,6 +16,8 @@ exception IncludedFileNotCompiled of string * string
 
 let magic = 2;;
 
+let prerr_endline _ = ()
+
 let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
 
 let refresh_uri_in_universe =
@@ -79,7 +81,12 @@ let require_path path =
 
 let require0 user ~baseuri = require_path (ng_path_of_baseuri user baseuri)
 
-let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
+let db_path user =
+ let midpath = match user with
+  | None -> ""
+  | Some u -> "/" ^ u
+ in
+ Helm_registry.get "matita.basedir" ^ midpath ^ "/ng_db.ng";;
 
 type timestamp =
  [ `Obj of NUri.uri * NCic.obj 
@@ -89,17 +96,35 @@ type timestamp =
 
 let time0 = [],[];;
 
+let global_aliases_db = ref [];;
+let rev_includes_map_db = ref [];;
+
+let global_aliases u = 
+  try List.assoc u !global_aliases_db
+  with Not_found -> 
+   let db = ref [] in
+   global_aliases_db := (u,db)::!global_aliases_db;
+   db
+;;
+
+let rev_includes_map u = 
+  try List.assoc u !rev_includes_map_db
+  with Not_found -> 
+   let db = ref NUri.UriMap.empty in
+   rev_includes_map_db := (u,db)::!rev_includes_map_db;
+   db
+;;
+
 let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
- let global_aliases = ref [] in
- let rev_includes_map = ref NUri.UriMap.empty in
- let store_db () =
-  let ch = open_out (db_path ()) in
-  Marshal.to_channel ch (magic,(!global_aliases,!rev_includes_map)) [];
+ let store_db user =
+  let ch = open_out (db_path user) in
+  Marshal.to_channel ch (magic,(!(global_aliases user),!(rev_includes_map user))) [];
   close_out ch in
- let load_db () =
+ let load_db user =
   HExtlib.mkdir (Helm_registry.get "matita.basedir");
+  if user <> None then HExtlib.mkdir ((Helm_registry.get "matita.basedir") ^ "/" ^ HExtlib.unopt user);
   try
-   let ga,im = require_path (db_path ()) in
+   let ga,im = require_path (db_path user) in
    let ga =
     List.map
      (fun (uri,name,NReference.Ref (uri2,spec)) ->
@@ -110,13 +135,13 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
      (fun u l im -> NUri.UriMap.add (refresh_uri u) (List.map refresh_uri l) im
      ) im NUri.UriMap.empty
    in
-    global_aliases := ga;
-    rev_includes_map := im
+    global_aliases user := ga;
+    rev_includes_map user := im
   with
    Sys_error _ -> () in
- let get_deps u =
+ let get_deps user u =
   let get_deps_one_step u =
-    try NUri.UriMap.find u !rev_includes_map with Not_found -> [] in
+    try NUri.UriMap.find u !(rev_includes_map user) with Not_found -> [] in
   let rec aux res =
    function
       [] -> res
@@ -127,19 +152,19 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
         aux (he::res) (get_deps_one_step he @ tl)
   in
    aux [] [u] in
- let remove_deps u =
-  rev_includes_map := NUri.UriMap.remove u !rev_includes_map;
-  rev_includes_map :=
+ let remove_deps user u =
+  rev_includes_map user := NUri.UriMap.remove u !(rev_includes_map user);
+  rev_includes_map user :=
    NUri.UriMap.map
-    (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !rev_includes_map;
-  store_db ()
+    (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !(rev_includes_map user);
+  store_db user
  in
   load_db,
-  (fun ga -> global_aliases := ga; store_db ()),
-  (fun () -> !global_aliases),
-  (fun u l ->
-    rev_includes_map := NUri.UriMap.add u (l @ get_deps u) !rev_includes_map;
-    store_db ()),
+  (fun user ga -> global_aliases user := ga; store_db user),
+  (fun user -> !(global_aliases user)),
+  (fun user u l ->
+    rev_includes_map user := NUri.UriMap.add u (l @ get_deps user u) !(rev_includes_map user);
+    store_db user),
   get_deps,
   remove_deps
 ;;
@@ -173,6 +198,11 @@ class virtual status uid =
   val timestamp = (time0 : timestamp)
   method timestamp = timestamp
 
+  method print_timestamp () = 
+    prerr_endline ("length(lib_db.storage) = " ^
+                   string_of_int (List.length !(lib_db.storage)));
+    prerr_endline ("length(timestamp.storage) = " ^
+                   string_of_int (List.length (fst timestamp)));
   method set_timestamp v = {< timestamp = v >}
   method set_lib_db v = {< lib_db = v >}
   method set_lib_status : 's.#g_status as 's -> 'self
@@ -185,6 +215,8 @@ let reset_timestamp st =
 ;;
 
 let time_travel0 st (sto,ali) =
+ prerr_endline ("length of lib_db.storage = " ^ (string_of_int (List.length !(st#lib_db.storage))));
+ prerr_endline ("length of sto = " ^ (string_of_int (List.length sto)));
  let diff_len = List.length !(st#lib_db.storage) - List.length sto in
  let to_be_deleted,_ = HExtlib.split_nth diff_len !(st#lib_db.storage) in
   if List.length to_be_deleted > 0 then
@@ -247,8 +279,8 @@ module type SerializerType =
  end
 
 module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
-  val set: dumpable_s -> dumpable_status -> dumpable_s (*val user : dumpable_s ->
-  string option*) end) =
+  val set: dumpable_s -> dumpable_status -> dumpable_s val user : dumpable_s ->
+  string option end) =
  struct
   type dumpable_status = D.dumpable_s
   type 'a register_type =
@@ -296,8 +328,9 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
          close_out ch
      | `Constr _ -> ()
     ) !((D.get status)#lib_db.storage);
-   set_global_aliases (!((D.get status)#lib_db.local_aliases) @ get_global_aliases ());
-   List.iter (fun u -> add_deps u [baseuri]) (D.get status)#dump.includes;
+   let user = D.user status in
+   set_global_aliases user (!((D.get status)#lib_db.local_aliases) @ get_global_aliases user);
+   List.iter (fun u -> add_deps (D.user status) u [baseuri]) (D.get status)#dump.includes;
    reset_timestamp (D.get status)
 
   let require2 ~baseuri ~alias_only status =
@@ -359,7 +392,7 @@ let resolve st name =
  try
   HExtlib.filter_map
    (fun (_,name',nref) -> if name'=name then Some nref else None)
-   (!(st#lib_db.local_aliases) @ get_global_aliases ())
+   (!(st#lib_db.local_aliases) @ get_global_aliases st#user)
  with
   Not_found -> 
    (prerr_endline ("can't resolve object " ^ name);