X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_library%2FnCicLibrary.mli;h=badf1788434b444efc4508bf75c658b7be574803;hb=48c011f52853dd106dbf9cbbd1b9da61277fba3b;hp=89e701fc16bc25e0b3d970e6fcdd5838b322ec24;hpb=6c702f5054d7975f76911ba62da9bfa33d3ed0fa;p=helm.git

diff --git a/matitaB/components/ng_library/nCicLibrary.mli b/matitaB/components/ng_library/nCicLibrary.mli
index 89e701fc1..badf17884 100644
--- a/matitaB/components/ng_library/nCicLibrary.mli
+++ b/matitaB/components/ng_library/nCicLibrary.mli
@@ -16,26 +16,41 @@ exception IncludedFileNotCompiled of string * string
 
 type timestamp
 
+type db
+
+class type g_status =
+  object
+    inherit NCicEnvironment.g_status
+    method lib_db : db
+  end
+
 class virtual status :
  string option ->
  object ('self)
-  inherit NCic.status
+  inherit NCicEnvironment.status
+  inherit g_status
+  method lib_db: db
   method timestamp: timestamp
+  method print_timestamp : unit -> unit
   method set_timestamp: timestamp -> 'self
+  method set_lib_db: db -> 'self
+  method set_lib_status: #g_status -> 'self
  end
 
 (* it also checks it and add it to the environment *)
 val add_obj: #status as 'status -> NCic.obj -> 'status
 val add_constraint: 
   #status as 'status -> NCic.universe -> NCic.universe -> 'status
-val aliases_of: NUri.uri -> NReference.reference list
-val resolve: string -> NReference.reference list
+val aliases_of: #status -> NUri.uri -> NReference.reference list
+val resolve: #status -> string -> NReference.reference list
+(*
 (* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *)
 val get_obj: #NCic.status -> NUri.uri -> NCic.obj (* changes the current timestamp *)
+*)
 
 val time_travel: #status -> unit
 
-val init: unit -> unit
+val init: string option -> unit
 
 type obj
 type dump
@@ -45,9 +60,12 @@ class type g_dumpable_status =
   method dump: dump
  end
 
-class dumpable_status : 
+class dumpable_status :
+ string option -> 
  object ('self)
   inherit g_dumpable_status
+  inherit NCicPp.status
+  inherit status
   method set_dump: dump -> 'self
   method set_dumpable_status: #g_dumpable_status -> 'self
  end
@@ -62,7 +80,7 @@ module type SerializerType =
   type 'a register_type =
    'a ->
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
-    refresh_uri_in_term:(NCic.status -> NCic.term -> NCic.term) ->
+    refresh_uri_in_term:(NCicEnvironment.status -> NCic.term -> NCic.term) ->
     refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
     alias_only:bool ->
      dumpable_status -> dumpable_status