This commit patches the environment and the library so that their status is

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

diff --git a/matitaB/components/ng_library/nCicLibrary.mli b/matitaB/components/ng_library/nCicLibrary.mli
index 89e701fc16bc25e0b3d970e6fcdd5838b322ec24..cba90c30cb10e932ba286a93ecbff287cd0e9985 100644 (file)
--- a/matitaB/components/ng_library/nCicLibrary.mli
+++ b/matitaB/components/ng_library/nCicLibrary.mli
@@ -16,22 +16,35 @@ exception IncludedFileNotCompiled of string * string
 
 type timestamp
 
+type db
+
+class type g_status =
+  object
+    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 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
 
@@ -45,9 +58,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 +78,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