(* $Id$ *)
-exception ObjectNotFound of string Lazy.t
exception LibraryOutOfSync of string Lazy.t
type timestamp
-val time0: timestamp
-val add_obj: NUri.uri -> NCic.obj -> timestamp
+class status :
+ object ('self)
+ method timestamp: timestamp
+ method set_timestamp: timestamp -> 'self
+ method set_library_status: <timestamp: timestamp; ..> -> '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 -> bool -> NCic.universe -> NCic.universe -> 'status
val aliases_of: NUri.uri -> NReference.reference list
val resolve: string -> NReference.reference list
+(* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *)
val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *)
val clear_cache : unit -> unit
-val time_travel: timestamp -> unit
+val time_travel: #status -> unit
val decompile: baseuri:NUri.uri -> unit
module type Serializer =
sig
type status
type obj
- val register: string -> ('a -> status -> status) -> ('a -> obj)
+ val register:
+ string ->
+ ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) ->
+ ('a -> obj)
val serialize: baseuri:NUri.uri -> obj list -> unit
val require: baseuri:NUri.uri -> status -> status
end
module Serializer(S: sig type status end): Serializer with type status= S.status
+val init: unit -> unit
+
+(* CSC: only required during old-to-NG phase, to be deleted *)
+val refresh_uri: NUri.uri -> NUri.uri
+
(* EOF *)