X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_library%2FnCicLibrary.mli;h=badf1788434b444efc4508bf75c658b7be574803;hb=41b61472d2c475e0f69e3dfc85539da3ad2bac1e;hp=63bd7518aa538421c45131e0adee55ba9fc8a82c;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/ng_library/nCicLibrary.mli b/matitaB/components/ng_library/nCicLibrary.mli
index 63bd7518a..badf17884 100644
--- a/matitaB/components/ng_library/nCicLibrary.mli
+++ b/matitaB/components/ng_library/nCicLibrary.mli
@@ -16,25 +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,8 +61,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 +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
@@ -71,13 +90,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 *)