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

[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 92c57b12391f960ec09f6693c3d364ef5b50e83c..a8215ab6a1797cbdcf29aaa1aa34ffa1ae917d8e 100644 (file)
--- a/matitaB/components/ng_library/nCicLibrary.ml
+++ b/matitaB/components/ng_library/nCicLibrary.ml
@@ -51,9 +51,13 @@ let refresh_uri_in_obj status (uri,height,metasenv,subst,obj_kind) =
   NCicUntrusted.map_obj_kind (refresh_uri_in_term status) obj_kind
 ;;
 
-let ng_path_of_baseuri ?(no_suffix=false) baseuri =
+let ng_path_of_baseuri ?(no_suffix=false) user baseuri =
  let uri = NUri.string_of_uri baseuri in
  let path = String.sub uri 4 (String.length uri - 4) in
+ let path = match user with
+ | Some u -> "/" ^ u ^ path
+ | _ -> path
+ in
  let path = Helm_registry.get "matita.basedir" ^ path in
  let dirname = Filename.dirname path in
   HExtlib.mkdir dirname;
@@ -73,7 +77,7 @@ let require_path path =
    dump
 ;;
 
-let require0 ~baseuri = require_path (ng_path_of_baseuri baseuri)
+let require0 user ~baseuri = require_path (ng_path_of_baseuri user baseuri)
 
 let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
 
@@ -144,9 +148,9 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
 
 let init = load_db;;
 
-class virtual status =
+class virtual status uid =
  object
-  inherit NCic.status
+  inherit NCic.status uid
   val timestamp = (time0 : timestamp)
   method timestamp = timestamp
   method set_timestamp v = {< timestamp = v >}
@@ -172,6 +176,7 @@ class type g_dumpable_status =
   method dump: dump
  end
 
+(* uid = None --> single user mode *)
 class dumpable_status =
  object
   val db = { objs = []; includes = []; dependencies = [] }
@@ -207,10 +212,12 @@ module type SerializerType =
   val require:
    baseuri:NUri.uri -> fname:string -> alias_only:bool ->
     dumpable_status -> dumpable_status
-  val dependencies_of: baseuri:NUri.uri -> string list
+  val dependencies_of: string option -> baseuri:NUri.uri -> string list
  end
 
-module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status  val set: dumpable_s -> dumpable_status -> dumpable_s 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) =
  struct
   type dumpable_status = D.dumpable_s
   type 'a register_type =
@@ -245,20 +252,19 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
    end
 
   let serialize ~baseuri status =
-   let status = D.get status in
-   let ch = open_out (ng_path_of_baseuri baseuri) in
-   Marshal.to_channel ch (magic,(status#dump.dependencies,status#dump.objs)) [];
+   let ch = open_out (ng_path_of_baseuri (D.user status) baseuri) in
+   Marshal.to_channel ch (magic,((D.get status)#dump.dependencies,(D.get status)#dump.objs)) [];
    close_out ch;
    List.iter
     (function 
      | `Obj (uri,obj) ->
-         let ch = open_out (ng_path_of_baseuri uri) in
+         let ch = open_out (ng_path_of_baseuri (D.user status) uri) in
          Marshal.to_channel ch (magic,obj) [];
          close_out ch
      | `Constr _ -> ()
     ) !storage;
    set_global_aliases (!local_aliases @ get_global_aliases ());
-   List.iter (fun u -> add_deps u [baseuri]) status#dump.includes;
+   List.iter (fun u -> add_deps u [baseuri]) (D.get status)#dump.includes;
    time_travel0 time0
 
   let require2 ~baseuri ~alias_only status =
@@ -269,13 +275,13 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
       (s#set_dump
         {s#dump with
         includes = baseuri::List.filter ((<>) baseuri) s#dump.includes}) in
-    let _dependencies,dump = require0 ~baseuri in
+    let _dependencies,dump = require0 (D.user status) ~baseuri in
      List.fold_right (!require1 ~alias_only) dump status
    with
     Sys_error _ ->
-     raise (IncludedFileNotCompiled(ng_path_of_baseuri baseuri,NUri.string_of_uri baseuri))
+     raise (IncludedFileNotCompiled(ng_path_of_baseuri (D.user status) baseuri,NUri.string_of_uri baseuri))
 
-  let dependencies_of ~baseuri = fst (require0 ~baseuri)
+  let dependencies_of user ~baseuri = fst (require0 user ~baseuri)
 
   let record_include =
    let aux (baseuri,fname) ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_
@@ -311,8 +317,8 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
          objs = record_include (baseuri,fname)::s#dump.objs })
 end
 
-let fetch_obj status uri =
- let obj = require0 ~baseuri:uri in
+let fetch_obj user status uri =
+ let obj = require0 user ~baseuri:uri in
   refresh_uri_in_obj status obj
 ;;
 
@@ -386,7 +392,7 @@ let get_obj status u =
     (function `Obj (u,o) -> Some (u,o) | _ -> None )
     !storage)
  with Not_found ->
-  try fetch_obj status u
+  try fetch_obj (status#user) status u
   with Sys_error _ ->
    raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u)))
 ;;