]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicLibrary.mli
EXPERIMENTAL COMMIT (by CSC,actuall :-)
[helm.git] / helm / software / components / ng_kernel / nCicLibrary.mli
index fe3262109bd7ba9d93054e25ed73832484d60436..11a608e1da89af9471780685a8e04ba6833bbe43 100644 (file)
 (* $Id$ *)
 
 exception ObjectNotFound of string Lazy.t
+exception LibraryOutOfSync of string Lazy.t
 
-val add_obj: NUri.uri -> NCic.obj -> unit
+type timestamp
+val time0: timestamp
+
+val add_obj: NUri.uri -> NCic.obj -> timestamp
 val aliases_of: NUri.uri -> NReference.reference list
 val resolve: string -> NReference.reference list
-val get_obj: NUri.uri -> NCic.obj
+val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *)
 
 val clear_cache : unit -> unit
 
+val time_travel: timestamp -> unit
+val serialize: baseuri:NUri.uri -> ('status -> 'status) -> unit
+val require: baseuri:NUri.uri -> 'status -> 'status
+val decompile: baseuri:NUri.uri -> unit
+
 (* EOF *)