From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 10 Jun 2011 12:56:04 +0000 (+0000)
Subject: Multi-user matita: changed the status object to include a ``user'' method
X-Git-Tag: make_still_working~2445
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6c702f5054d7975f76911ba62da9bfa33d3ed0fa;p=helm.git

Multi-user matita: changed the status object to include a ``user'' method
containing an optional string, used to identify associated user.
---

diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml
index 7361bf599..627291880 100644
--- a/matitaB/components/content_pres/cicNotationParser.ml
+++ b/matitaB/components/content_pres/cicNotationParser.ml
@@ -782,7 +782,7 @@ EXTEND
                 (* CSC: new NCicPp.status is the best I can do here
                    without changing the return type *)
                 Ast.fail loc (sprintf "Argument %s not found"
-                  (NotationPp.pp_term (new NCicPp.status) name))
+                  (NotationPp.pp_term (new NCicPp.status None) name))
             | (l,_) :: tl -> 
                 (match position_of name 0 l with
                 | None, len -> find_arg name (n + len) tl
@@ -961,9 +961,9 @@ class status0 ~keywords:kwds =
     db.loctable := CicNotationLexer.LocalizeEnv.empty
  end
 
-class virtual status ~keywords:kwds =
+class virtual status uid ~keywords:kwds =
  object
-  inherit NCic.status
+  inherit NCic.status uid
   inherit status0 kwds
  end
 
diff --git a/matitaB/components/content_pres/cicNotationParser.mli b/matitaB/components/content_pres/cicNotationParser.mli
index f5daf20b0..d711a3067 100644
--- a/matitaB/components/content_pres/cicNotationParser.mli
+++ b/matitaB/components/content_pres/cicNotationParser.mli
@@ -33,7 +33,7 @@ class type g_status =
   method notation_parser_db: db
  end
 
-class virtual status: keywords:string list ->
+class virtual status: string option -> keywords:string list ->
  object('self)
   inherit NCic.status
   inherit g_status
diff --git a/matitaB/components/content_pres/content2presMatcher.ml b/matitaB/components/content_pres/content2presMatcher.ml
index a7b59aa52..5eeed2667 100644
--- a/matitaB/components/content_pres/content2presMatcher.ml
+++ b/matitaB/components/content_pres/content2presMatcher.ml
@@ -71,8 +71,9 @@ struct
 
     (* Debugging only *)
     (*CSC: new NCicPp.status is the best I can do now *)
-    let string_of_term = NotationPp.pp_term (new NCicPp.status)
-    let string_of_pattern = NotationPp.pp_term (new NCicPp.status)
+    (*WR: can't guess a user id so I must use None *)
+    let string_of_term = NotationPp.pp_term (new NCicPp.status None)
+    let string_of_pattern = NotationPp.pp_term (new NCicPp.status None)
   end
 
   module M = PatternMatcher.Matcher (Pattern21)
diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index 8ff5a13f2..d724acf85 100644
--- a/matitaB/components/content_pres/termContentPres.ml
+++ b/matitaB/components/content_pres/termContentPres.ml
@@ -317,9 +317,9 @@ class type g_status =
     method content_pres_db: db
   end
  
-class virtual status =
+class virtual status uid =
  object
-   inherit NCic.status
+   inherit NCic.status uid
    val content_pres_db = initial_db  
    method content_pres_db = content_pres_db
    method set_content_pres_db v = {< content_pres_db = v >}
diff --git a/matitaB/components/content_pres/termContentPres.mli b/matitaB/components/content_pres/termContentPres.mli
index 4d0bb909b..34e63aa64 100644
--- a/matitaB/components/content_pres/termContentPres.mli
+++ b/matitaB/components/content_pres/termContentPres.mli
@@ -33,6 +33,7 @@ class type g_status =
   end
 
 class virtual status :
+  string option ->
   object ('self)
     inherit NCic.status
     method content_pres_db: db
diff --git a/matitaB/components/grafite_engine/grafiteTypes.ml b/matitaB/components/grafite_engine/grafiteTypes.ml
index bfbb982c7..5b34158c4 100644
--- a/matitaB/components/grafite_engine/grafiteTypes.ml
+++ b/matitaB/components/grafite_engine/grafiteTypes.ml
@@ -31,19 +31,19 @@ exception Command_error of string
 
 let command_error msg = raise (Command_error msg)
 
-class virtual status = fun (b : string) ->
+class virtual status = fun (uid : string option) (b : string) ->
  let fake_obj =
   NUri.uri_of_string "cic:/matita/dummy.decl",0,[],[],
    NCic.Constant([],"",None,NCic.Implicit `Closed,(`Provided,`Theorem,`Regular))
  in
   object
    (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
-   inherit ([Continuationals.Stack.t] NTacStatus.status fake_obj (Continuationals.Stack.empty))
+   inherit ([Continuationals.Stack.t] NTacStatus.status uid fake_obj (Continuationals.Stack.empty))
    inherit NCicLibrary.dumpable_status
-   inherit NCicLibrary.status
-   inherit GrafiteDisambiguate.status
-   inherit GrafiteParser.status
-   inherit TermContentPres.status
+   inherit NCicLibrary.status uid
+   inherit GrafiteDisambiguate.status uid
+   inherit GrafiteParser.status uid
+   inherit TermContentPres.status uid
    val baseuri = b
    val ng_mode = (`CommandMode : [`CommandMode | `ProofMode])
    method baseuri = baseuri
@@ -57,4 +57,5 @@ module Serializer =
   type dumpable_s = status
   let get status = (status : #status :> NCicLibrary.dumpable_status)
   let set (status : dumpable_s) dump_status = status#set_dumpable_status dump_status
+  let user (status : dumpable_s) = status#user
  end)
diff --git a/matitaB/components/grafite_engine/grafiteTypes.mli b/matitaB/components/grafite_engine/grafiteTypes.mli
index 90fdbb52e..0351b2611 100644
--- a/matitaB/components/grafite_engine/grafiteTypes.mli
+++ b/matitaB/components/grafite_engine/grafiteTypes.mli
@@ -32,7 +32,7 @@ exception Command_error of string
 val command_error: string -> 'a   (** @raise Command_error *)
 
 class virtual status :
- string ->
+ string option -> string ->
   object ('self)
    (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *)
    inherit NTacStatus.tac_status
diff --git a/matitaB/components/grafite_parser/grafiteParser.ml b/matitaB/components/grafite_parser/grafiteParser.ml
index ca2224ff5..30a97a3e3 100644
--- a/matitaB/components/grafite_parser/grafiteParser.ml
+++ b/matitaB/components/grafite_parser/grafiteParser.ml
@@ -169,7 +169,8 @@ EXTEND
       | _ ->
        (*CSC: new NCicPp.status is the best I can do here without changing the
          result type *)
-       raise (Invalid_argument ("malformed target parameter list 2\n" ^ NotationPp.pp_term (new NCicPp.status) params)) ]
+       raise (Invalid_argument ("malformed target parameter list 2\n" ^
+              NotationPp.pp_term (new NCicPp.status None ) params)) ]
   ];
   direction: [
     [ SYMBOL ">" -> `LeftToRight
@@ -640,9 +641,9 @@ class type g_status =
   method parser_db: db
  end
 
-class virtual status =
+class virtual status uid =
  object(self)
-  inherit CicNotationParser.status ~keywords:[]
+  inherit CicNotationParser.status uid ~keywords:[]
   val mutable db = None (* mutable only to initialize it :-( *)
   method parser_db = match db with None -> assert false | Some x -> x
   method set_parser_db v = {< db = Some v >}
diff --git a/matitaB/components/grafite_parser/grafiteParser.mli b/matitaB/components/grafite_parser/grafiteParser.mli
index aa0fb5bde..4f3ce988e 100644
--- a/matitaB/components/grafite_parser/grafiteParser.mli
+++ b/matitaB/components/grafite_parser/grafiteParser.mli
@@ -32,6 +32,7 @@ class type g_status =
  end
 
 class virtual status :
+ string option ->
  object('self)
   inherit g_status
   inherit CicNotationParser.status
diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml
index 75f469430..ed2b58a79 100644
--- a/matitaB/components/ng_cic_content/interpretations.ml
+++ b/matitaB/components/ng_cic_content/interpretations.ml
@@ -67,9 +67,9 @@ class type g_status =
     method interp_db: db
   end
  
-class virtual status =
+class virtual status uid =
  object(self)
-   inherit NCicCoercion.status
+   inherit NCicCoercion.status uid
    val mutable interp_db = None (* mutable only to initialize it :-( *)
    method interp_db = match interp_db with None -> assert false | Some x -> x
    method set_interp_db v = {< interp_db = Some v >}
diff --git a/matitaB/components/ng_cic_content/interpretations.mli b/matitaB/components/ng_cic_content/interpretations.mli
index 4665be92c..122096799 100644
--- a/matitaB/components/ng_cic_content/interpretations.mli
+++ b/matitaB/components/ng_cic_content/interpretations.mli
@@ -37,6 +37,7 @@ class type g_status =
   end
 
 class virtual status :
+  string option ->
   object ('self)
     inherit g_status
     inherit NCicCoercion.status
diff --git a/matitaB/components/ng_cic_content/ncic2astMatcher.ml b/matitaB/components/ng_cic_content/ncic2astMatcher.ml
index 4f65e9c03..1c71db8c5 100644
--- a/matitaB/components/ng_cic_content/ncic2astMatcher.ml
+++ b/matitaB/components/ng_cic_content/ncic2astMatcher.ml
@@ -61,8 +61,10 @@ struct
 
     (* Debugging functions only *)
     let string_of_pattern = NotationPp.pp_cic_appl_pattern
+
+    (* WR: hope it's safe to pass userid=None to NCicPp.status *)
     let string_of_term t =
-     (new NCicPp.status)#ppterm ~metasenv:[] ~subst:[] ~context:[] t
+     (new NCicPp.status None)#ppterm ~metasenv:[] ~subst:[] ~context:[] t
 
     let classify = function
       | Ast.ImplicitPattern
diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
index 0cadc45b7..30bd9b834 100644
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -51,9 +51,9 @@ class type g_status =
    method disambiguate_db: db
   end
 
-class virtual status =
+class virtual status uid =
  object (self)
-  inherit Interpretations.status
+  inherit Interpretations.status uid
   val disambiguate_db = initial_status
   method disambiguate_db = disambiguate_db
   method set_disambiguate_db v = {< disambiguate_db = v >}
diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli
index 0babba272..b88bc0e1d 100644
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli
@@ -32,6 +32,7 @@ class type g_status =
  end
 
 class virtual status :
+  string option ->
  object ('self)
   inherit g_status
   inherit Interpretations.status
diff --git a/matitaB/components/ng_kernel/nCic.ml b/matitaB/components/ng_kernel/nCic.ml
index 7e4e4f855..271bf5284 100644
--- a/matitaB/components/ng_kernel/nCic.ml
+++ b/matitaB/components/ng_kernel/nCic.ml
@@ -121,8 +121,10 @@ type obj_kind =
 type obj = NUri.uri * int * metasenv * substitution * obj_kind
 
 (* pretty-printing *)
-class virtual status =
+class virtual status (uid : string option) =
  object
+  method user = uid
+
   method virtual ppterm: context:context -> subst:substitution ->
    metasenv:metasenv -> ?margin:int -> ?inside_fix:bool -> term -> string
 
diff --git a/matitaB/components/ng_kernel/nCicEnvironment.ml b/matitaB/components/ng_kernel/nCicEnvironment.ml
index c7389f167..1b155a030 100644
--- a/matitaB/components/ng_kernel/nCicEnvironment.ml
+++ b/matitaB/components/ng_kernel/nCicEnvironment.ml
@@ -24,7 +24,7 @@ let cache = NUri.UriHash.create 313;;
 let history = ref [];;
 let frozen_list = ref [];;
 
-let get_obj = ref (fun _ _ -> assert false);;
+let get_obj = ref (fun _ _ -> assert false) ;;
 let set_get_obj = (:=) get_obj;;
 
 module F = Format 
diff --git a/matitaB/components/ng_kernel/nCicPp.ml b/matitaB/components/ng_kernel/nCicPp.ml
index 0d78c4971..84c95f45a 100644
--- a/matitaB/components/ng_kernel/nCicPp.ml
+++ b/matitaB/components/ng_kernel/nCicPp.ml
@@ -359,9 +359,10 @@ let ppsubst status ~metasenv ?use_subst subst =
 
 let ppobj status obj = on_buffer (ppobj status) obj;;
 
-class status =
+class status (uid : string option) =
  object(self)
   (* this method is meant to be overridden in ApplyTransformation *)
+  method user = uid
   method ppterm = ppterm self
   method ppcontext = ppcontext self
   method ppmetasenv = ppmetasenv self
diff --git a/matitaB/components/ng_kernel/nCicPp.mli b/matitaB/components/ng_kernel/nCicPp.mli
index 02b6c8642..06be5b261 100644
--- a/matitaB/components/ng_kernel/nCicPp.mli
+++ b/matitaB/components/ng_kernel/nCicPp.mli
@@ -17,7 +17,7 @@ val string_of_flavour: NCic.def_flavour -> string
 
 (* low-level pretty printer;
    all methods are meant to be overridden in ApplyTransformation *)
-class status: NCic.cstatus
+class status: string option -> NCic.cstatus
 
 (* variants that use a formatter 
 module Format : sig
diff --git a/matitaB/components/ng_library/nCicLibrary.ml b/matitaB/components/ng_library/nCicLibrary.ml
index 92c57b123..a8215ab6a 100644
--- 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)))
 ;;
diff --git a/matitaB/components/ng_library/nCicLibrary.mli b/matitaB/components/ng_library/nCicLibrary.mli
index 63bd7518a..89e701fc1 100644
--- a/matitaB/components/ng_library/nCicLibrary.mli
+++ b/matitaB/components/ng_library/nCicLibrary.mli
@@ -17,6 +17,7 @@ exception IncludedFileNotCompiled of string * string
 type timestamp
 
 class virtual status :
+ string option ->
  object ('self)
   inherit NCic.status
   method timestamp: timestamp
@@ -44,7 +45,7 @@ class type g_dumpable_status =
   method dump: dump
  end
 
-class dumpable_status :
+class dumpable_status : 
  object ('self)
   inherit g_dumpable_status
   method set_dump: dump -> 'self
@@ -71,13 +72,15 @@ 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) :
-  SerializerType with type dumpable_status = D.dumpable_s
+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) :
+ SerializerType with type dumpable_status = D.dumpable_s
 
 val refresh_uri: NUri.uri -> NUri.uri
 
-val ng_path_of_baseuri: ?no_suffix:bool -> NUri.uri -> string
+val ng_path_of_baseuri: ?no_suffix:bool -> string option -> NUri.uri -> string
 (* EOF *)
diff --git a/matitaB/components/ng_paramodulation/nCicBlob.ml b/matitaB/components/ng_paramodulation/nCicBlob.ml
index b9314a203..cd944c43d 100644
--- a/matitaB/components/ng_paramodulation/nCicBlob.ml
+++ b/matitaB/components/ng_paramodulation/nCicBlob.ml
@@ -80,7 +80,8 @@ with type t = NCic.term and type input = NCic.term = struct
   
   let compare x y = 
     (* CSC: NCicPp.status is the best I can put here *)
-    if NCicReduction.alpha_eq (new NCicPp.status) [] [] [] x y  then 0 
+    (* WR: and I can't guess a user id, so I must put None *)
+    if NCicReduction.alpha_eq (new NCicPp.status None) [] [] [] x y  then 0 
     (* if x = y  then 0 *)
     else compare x y
   ;;
@@ -99,7 +100,8 @@ with type t = NCic.term and type input = NCic.term = struct
 
   let pp t = 
     (* CSC: NCicPp.status is the best I can put here *)
-    (new NCicPp.status)#ppterm ~context:C.context
+    (* WR: and I can't guess a user id, so I must put None *)
+    (new NCicPp.status None)#ppterm ~context:C.context
       ~metasenv:C.metasenv ~subst:C.subst t;;
 
   type input = NCic.term
@@ -122,7 +124,8 @@ with type t = NCic.term and type input = NCic.term = struct
   let saturate t ty = 
     let sty, _, args = 
       (* CSC: NCicPp.status is the best I can put here *)
-      NCicMetaSubst.saturate (new NCicPp.status) ~delta:0 C.metasenv C.subst
+      (* WR: and I can't guess a user id, so I must put None *)
+      NCicMetaSubst.saturate (new NCicPp.status None) ~delta:0 C.metasenv C.subst
        C.context ty 0
     in
     let proof = 
diff --git a/matitaB/components/ng_refiner/nCicCoercion.ml b/matitaB/components/ng_refiner/nCicCoercion.ml
index cfb9d1b6b..79d050bc0 100644
--- a/matitaB/components/ng_refiner/nCicCoercion.ml
+++ b/matitaB/components/ng_refiner/nCicCoercion.ml
@@ -39,9 +39,9 @@ class type g_status =
   method coerc_db: db
  end
 
-class virtual status =
+class virtual status uid =
  object
-  inherit NCicUnifHint.status
+  inherit NCicUnifHint.status uid
   val db = empty_db
   method coerc_db = db
   method set_coerc_db v = {< db = v >}
diff --git a/matitaB/components/ng_refiner/nCicCoercion.mli b/matitaB/components/ng_refiner/nCicCoercion.mli
index 4f1fa4186..7c32ba1e0 100644
--- a/matitaB/components/ng_refiner/nCicCoercion.mli
+++ b/matitaB/components/ng_refiner/nCicCoercion.mli
@@ -20,6 +20,7 @@ class type g_status =
  end
 
 class virtual status :
+ string option ->
  object ('self)
   inherit g_status
   inherit NCicUnifHint.status
diff --git a/matitaB/components/ng_refiner/nCicUnifHint.ml b/matitaB/components/ng_refiner/nCicUnifHint.ml
index ff8de7554..960ead117 100644
--- a/matitaB/components/ng_refiner/nCicUnifHint.ml
+++ b/matitaB/components/ng_refiner/nCicUnifHint.ml
@@ -51,9 +51,9 @@ class type g_status =
   method uhint_db: db
  end
 
-class virtual status =
+class virtual status (uid : string option) =
  object
-  inherit NCic.status
+  inherit NCic.status uid
   val db = HDB.empty, EQDB.empty
   method uhint_db = db
   method set_uhint_db v = {< db = v >}
diff --git a/matitaB/components/ng_refiner/nCicUnifHint.mli b/matitaB/components/ng_refiner/nCicUnifHint.mli
index 832e980e2..77600663a 100644
--- a/matitaB/components/ng_refiner/nCicUnifHint.mli
+++ b/matitaB/components/ng_refiner/nCicUnifHint.mli
@@ -21,6 +21,7 @@ class type g_status =
  end
 
 class virtual status :
+ string option ->
  object ('self)
   inherit g_status
   inherit NCic.status
diff --git a/matitaB/components/ng_tactics/nTacStatus.ml b/matitaB/components/ng_tactics/nTacStatus.ml
index 9a6358baa..3684c051f 100644
--- a/matitaB/components/ng_tactics/nTacStatus.ml
+++ b/matitaB/components/ng_tactics/nTacStatus.ml
@@ -72,10 +72,10 @@ class type g_pstatus =
   method obj: NCic.obj
  end
 
-class virtual pstatus =
+class virtual pstatus uid =
  fun (o: NCic.obj) ->
  object (self)
-   inherit GrafiteDisambiguate.status
+   inherit GrafiteDisambiguate.status uid
    inherit auto_status
    inherit eq_status
    val obj = o
@@ -479,10 +479,10 @@ class type ['stack] g_status =
   method stack: 'stack
  end
 
-class virtual ['stack] status =
+class virtual ['stack] status uid =
  fun (o: NCic.obj) (s: 'stack) ->
  object (self)
-   inherit (pstatus o)
+   inherit (pstatus uid o)
    val stack = s
    method stack = stack
    method set_stack s = {< stack = s >}
diff --git a/matitaB/components/ng_tactics/nTacStatus.mli b/matitaB/components/ng_tactics/nTacStatus.mli
index 35e74debf..f2a128665 100644
--- a/matitaB/components/ng_tactics/nTacStatus.mli
+++ b/matitaB/components/ng_tactics/nTacStatus.mli
@@ -50,7 +50,7 @@ class type g_pstatus =
  end
 
 class virtual pstatus :
- NCic.obj ->
+ string option -> NCic.obj ->
   object ('self)
    inherit g_pstatus
    inherit GrafiteDisambiguate.status
@@ -128,7 +128,7 @@ class type ['stack] g_status =
  end
 
 class virtual ['stack] status :
- NCic.obj -> 'stack ->
+ string option -> NCic.obj -> 'stack ->
   object ('self)
    inherit ['stack] g_status
    inherit pstatus
diff --git a/matitaB/components/ng_tactics/nTactics.ml b/matitaB/components/ng_tactics/nTactics.ml
index aecc88e1f..889b8b309 100644
--- a/matitaB/components/ng_tactics/nTactics.ml
+++ b/matitaB/components/ng_tactics/nTactics.ml
@@ -205,9 +205,10 @@ let compare_statuses ~past ~present =
 (* CSC: potential bug here: the new methods still use the instance variables
    of the old status and not the instance variables of the new one *)
 let change_stack_type (status : 'a #NTacStatus.status) (stack: 'b) : 'b NTacStatus.status =
+ let uid = status#user in
  let o =
   object
-   inherit ['b] NTacStatus.status status#obj stack
+   inherit ['b] NTacStatus.status uid status#obj stack
    method ppterm = status#ppterm
    method ppcontext = status#ppcontext
    method ppsubst = status#ppsubst
diff --git a/matitaB/configure.ac b/matitaB/configure.ac
index e11e011a0..39822d14e 100644
--- a/matitaB/configure.ac
+++ b/matitaB/configure.ac
@@ -92,14 +92,13 @@ $FINDLIB_CREQUIRES \
 lablgtk2.glade \
 lablgtksourceview2.gtksourceview2 \
 "
-# FIXME: we currently depend from some GTK libraries
-# this should be fixed!!!
 FINDLIB_WREQUIRES="\
 $FINDLIB_CREQUIRES \
 netcgi2 \
 nethttpd \
+uuidm \
 "
-for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES
+for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES $FINDLIB_WREQUIRES
 do
   AC_MSG_CHECKING(for $r ocaml library)
   if OCAMLPATH=$OCAMLPATH $OCAMLFIND query $r &> /dev/null; then
diff --git a/matitaB/matita/.depend b/matitaB/matita/.depend
index 75f3da02b..655c76266 100644
--- a/matitaB/matita/.depend
+++ b/matitaB/matita/.depend
@@ -8,12 +8,16 @@ cicMathView.cmx: matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
     buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi 
 lablGraphviz.cmo: lablGraphviz.cmi 
 lablGraphviz.cmx: lablGraphviz.cmi 
+matitaAuthentication.cmo: matitaEngine.cmi matitaAuthentication.cmi 
+matitaAuthentication.cmx: matitaEngine.cmx matitaAuthentication.cmi 
 matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi 
 matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi 
 matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaEngine.cmi 
 matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx 
-matitadaemon.cmo: matitaGtkMisc.cmi matitaEngine.cmi applyTransformation.cmi 
-matitadaemon.cmx: matitaGtkMisc.cmx matitaEngine.cmx applyTransformation.cmx 
+matitadaemon.cmo: matitaInit.cmi matitaEngine.cmi matitaAuthentication.cmi \
+    applyTransformation.cmi 
+matitadaemon.cmx: matitaInit.cmx matitaEngine.cmx matitaAuthentication.cmx \
+    applyTransformation.cmx 
 matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi 
 matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi 
 matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi 
@@ -61,6 +65,7 @@ virtuals.cmx: virtuals.cmi
 applyTransformation.cmi: 
 cicMathView.cmi: matitaGuiTypes.cmi applyTransformation.cmi 
 lablGraphviz.cmi: 
+matitaAuthentication.cmi: matitaEngine.cmi 
 matitaclean.cmi: 
 matitaEngine.cmi: applyTransformation.cmi 
 matitaExcPp.cmi: 
diff --git a/matitaB/matita/Makefile b/matitaB/matita/Makefile
index 05e632427..3634caf65 100644
--- a/matitaB/matita/Makefile
+++ b/matitaB/matita/Makefile
@@ -3,7 +3,7 @@ export SHELL=/bin/bash
 include ../Makefile.defs
 
 NULL =
-#H=@
+H=@
 
 ifeq ($(ANNOT),true)
   ANNOTOPTION = -dtypes
@@ -67,6 +67,7 @@ MAINCMLI =			\
 ML = buildTimeConf.ml matitaGeneratedGui.ml $(MLI:%.mli=%.ml)
 # objects for matitac (batch compiler)
 CML = buildTimeConf.ml $(CMLI:%.mli=%.ml)
+WML = matitaAuthentication.ml $(CML)
 MAINCML = $(MAINCMLI:%.mli=%.ml)
 
 PROGRAMS_BYTE = \
@@ -84,11 +85,20 @@ ULEXDIR := $(shell $(OCAMLFIND) query ulex08)
 
 matitaScriptLexer.cmo: SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc"
 
+matitaAuthentication.cmi: matitaAuthentication.mli
+	$(H)echo "  OCAMLC $<"
+	$(H)$(OCAMLC) $(WPKGS) -c $<
+matitaAuthentication.cmo: matitaAuthentication.ml
+	$(H)echo "  OCAMLC $<"
+	$(H)$(OCAMLC) $(WPKGS) -c $<
+
 CMOS = $(ML:%.ml=%.cmo)
 CCMOS = $(CML:%.ml=%.cmo)
+WCMOS = $(WML:%.ml=%.cmo)
 MAINCMOS = $(MAINCML:%.ml=%.cmo)
 CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
 CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
+WCMXS = $(patsubst %.cmo,%.cmx,$(WCMOS))
 MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS))
 $(CMOS) : $(LIB_DEPS)
 $(CMXOS): $(LIBX_DEPS)
@@ -124,7 +134,7 @@ linkonly:
 	$(H)echo "  OCAMLC matitac.ml"
 	$(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitac.ml
 	$(H)echo "  OCAMLC matitadaemon.ml"
-	$(H)$(OCAMLC) $(WPKGS) -linkpkg -o matitadaemon $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitadaemon.ml
+	$(H)$(OCAMLC) $(WPKGS) -linkpkg -o matitadaemon $(WCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitadaemon.ml
 
 .PHONY: linkonly
 matita: matita.ml $(LIB_DEPS) $(CMOS)
@@ -141,12 +151,12 @@ matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS)
 	$(H)echo "  OCAMLOPT $<"
 	$(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml
 
-matitadaemon: matitadaemon.ml $(WLIB_DEPS) $(CCMOS) $(MAINCMOS)
+matitadaemon: matitadaemon.ml $(WLIB_DEPS) $(WCMOS) $(MAINCMOS)
 	$(H)echo "  OCAMLC $<"
-	$(H)$(OCAMLC) $(WPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitadaemon.ml
-matitadaemon.opt: matitadaemon.ml $(WLIBX_DEPS) $(CCMXS) $(MAINCMXS)
+	$(H)$(OCAMLC) $(WPKGS) -linkpkg -o $@ $(WCMOS) $(MAINCMOS) matitadaemon.ml
+matitadaemon.opt: matitadaemon.ml $(WLIBX_DEPS) $(WCMXS) $(MAINCMXS)
 	$(H)echo "  OCAMLOPT $<"
-	$(H)$(OCAMLOPT) $(WPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitadaemon.ml
+	$(H)$(OCAMLOPT) $(WPKGS) -linkpkg -o $@ $(WCMXS) $(MAINCMXS) matitadaemon.ml
 
 rottener: rottener.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS)
 	$(H)echo "  OCAMLC $<"
diff --git a/matitaB/matita/applyTransformation.ml b/matitaB/matita/applyTransformation.ml
index 5db35244e..0528a01ce 100644
--- a/matitaB/matita/applyTransformation.ml
+++ b/matitaB/matita/applyTransformation.ml
@@ -83,11 +83,11 @@ let ntxt_of_cic_subst ~map_unicode_to_tex size status ~metasenv ?use_subst subst
 *)
 
 
-class status =
+class status uid =
  object(self)
-  inherit Interpretations.status
-  inherit TermContentPres.status
-  inherit NCicPp.status
+  inherit Interpretations.status uid
+  inherit TermContentPres.status uid
+  inherit NCicPp.status uid
 (*
   method ppterm ~context ~subst ~metasenv ?margin ?inside_fix t =
     NCicPp.ppterm ~metasenv ~subst ~context t
diff --git a/matitaB/matita/applyTransformation.mli b/matitaB/matita/applyTransformation.mli
index 0aeec3f8c..5a399b663 100644
--- a/matitaB/matita/applyTransformation.mli
+++ b/matitaB/matita/applyTransformation.mli
@@ -36,6 +36,7 @@
 val use_high_level_pretty_printer: bool ref
 
 class status :
+ string option ->
  object
   inherit NCic.cstatus
   inherit Interpretations.status
diff --git a/matitaB/matita/matitaAuthentication.ml b/matitaB/matita/matitaAuthentication.ml
new file mode 100644
index 000000000..06e7d9451
--- /dev/null
+++ b/matitaB/matita/matitaAuthentication.ml
@@ -0,0 +1,96 @@
+(* Copyright (C) 2004-2011, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+type session_id = Uuidm.t
+
+(* user table: user id, (password, optional session id) *)
+type user = string * (string * session_id option)
+
+let user_tbl = (ref [] : user list ref)
+
+(* session table: (user id, session id), matita status *)
+type session = (string * session_id) * MatitaEngine.status 
+
+let session_tbl = (ref [] : session list ref)
+
+exception UsernameCollision of string
+
+let lookup_user uid = List.assoc uid !user_tbl
+
+let create_session uid status =
+  let pw,sid = List.assoc uid !user_tbl in
+  let clean_utbl = List.remove_assoc uid !user_tbl in
+  let new_session = Uuidm.create `V4 in
+  user_tbl := (uid,(pw,Some new_session))::clean_utbl;
+  let clean_stbl = match sid with
+    | Some sid' -> 
+       List.remove_assoc (uid,sid') !session_tbl
+    | _ -> !session_tbl
+  in session_tbl := ((uid,new_session),status)::clean_stbl
+;;
+
+let logout_user uid =
+  match List.assoc uid !user_tbl with
+  | _,None -> ()
+  | pw, Some sid ->
+     user_tbl := (uid,(pw,None))::List.remove_assoc uid !user_tbl;
+     session_tbl := List.remove_assoc (uid,sid) !session_tbl
+;;
+
+let remove_user uid =
+  user_tbl := List.remove_assoc uid !user_tbl
+;;
+
+(* serialization and deserialization of the user table *)
+let config_path () =
+  let path = Helm_registry.get "matita.basedir" in
+  let dirname = Filename.dirname path in
+  HExtlib.mkdir dirname;
+  path
+;;
+
+let serialize () =
+  let clean_utbl = List.map (fun (uid,(pw,_)) -> uid,(pw,None)) !user_tbl in
+  let utbl_ch = open_out (config_path () ^ "/usertable.dump") in
+  Marshal.to_channel utbl_ch clean_utbl [];
+  close_out utbl_ch;
+;;
+
+let deserialize () =
+  let utbl_ch = open_in (config_path () ^ "/usertable.dump") in
+  user_tbl := Marshal.from_channel utbl_ch;
+  close_in utbl_ch;
+  (* old_sessions are now invalid *)
+  session_tbl := [];
+;;
+
+let add_user uid pw =
+  try
+    let _ = lookup_user uid in
+    raise (UsernameCollision uid)
+  with Not_found -> 
+    user_tbl := (uid,(pw,None))::!user_tbl;
+    serialize ()
+;;
diff --git a/matitaB/matita/matitaAuthentication.mli b/matitaB/matita/matitaAuthentication.mli
new file mode 100644
index 000000000..ffbb206b7
--- /dev/null
+++ b/matitaB/matita/matitaAuthentication.mli
@@ -0,0 +1,42 @@
+(* Copyright (C) 2004-2011, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+type session_id = Uuidm.t
+
+exception UsernameCollision of string
+
+val lookup_user : string -> (string * session_id option)
+
+val create_session : string -> MatitaEngine.status -> unit
+
+val logout_user : string -> unit
+
+val remove_user : string -> unit
+
+val serialize : unit -> unit
+
+val deserialize : unit -> unit
+
+val add_user : string -> string -> unit
diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index 437121b73..9c86679bc 100644
--- 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 ->
diff --git a/matitaB/matita/matitaEngine.mli b/matitaB/matita/matitaEngine.mli
index ceffc6f7f..3bbc6a113 100644
--- a/matitaB/matita/matitaEngine.mli
+++ b/matitaB/matita/matitaEngine.mli
@@ -30,7 +30,7 @@ exception FailureCompiling of string * exn
 exception CircularDependency of string
 
 class status:
- string ->
+ string option -> string ->
   object
    inherit GrafiteTypes.status
    inherit ApplyTransformation.status
diff --git a/matitaB/matita/matitaScript.ml b/matitaB/matita/matitaScript.ml
index 5b794a6d8..69859470f 100644
--- a/matitaB/matita/matitaScript.ml
+++ b/matitaB/matita/matitaScript.ml
@@ -245,7 +245,8 @@ let source_buffer = source_view#source_buffer in
 let similarsymbols_tag_name = "similarsymbolos" in
 let similarsymbols_tag = `NAME similarsymbols_tag_name in
 let initial_statuses current baseuri =
- let status = new MatitaEngine.status baseuri in
+(* FIXME : currently hard coded to single user mode *)
+ let status = new MatitaEngine.status None baseuri in
  (match current with
      Some current ->
       NCicLibrary.time_travel status;
diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 3201771fe..8dbfa4511 100644
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -47,8 +47,8 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script
   (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*)
     utf8_length parsed_text
 
-
-let status = ref (new MatitaEngine.status "cic:/matita");;
+(* FIXME: currently hard coded to single user mode *)
+let status = ref (new MatitaEngine.status (Some "ricciott") "cic:/matita");;
 let history = ref [!status];;
 let sequent_size = ref 40;;
 
@@ -349,6 +349,10 @@ let start() =
                 ; "open", retrieve ]
       () in
   MatitaInit.initialize_all ();
+  (* test begin *)
+  MatitaAuthentication.add_user "ricciott" "pippo123";
+  MatitaAuthentication.add_user "asperti" "pluto456";
+  (* test end *)
   Netplex_main.startup
     parallelizer
     Netplex_log.logger_factories   (* allow all built-in logging styles *)