Fixes a bug (introduced in the previous revision) which caused the environment

[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 63bd7518aa538421c45131e0adee55ba9fc8a82c..b8453267aaf5522d270ab9561a762bcf99c5218f 100644 (file)
--- a/matitaB/components/ng_library/nCicLibrary.mli
+++ b/matitaB/components/ng_library/nCicLibrary.mli
@@ -16,21 +16,36 @@ 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 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,8 +60,11 @@ class type g_dumpable_status =
  end
 
 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
@@ -61,7 +79,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
@@ -71,13 +89,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 *)