Initial implementation of statuses using objects in place of nested records.

[helm.git] / helm / software / components / ng_kernel / nCicLibrary.mli

diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli
index 5266325656a7cdd14f21323a9d0201cf58d71be1..dfd17f15bd6303c242216e2c66d60d0948dcfbd5 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.mli
+++ b/helm/software/components/ng_kernel/nCicLibrary.mli
@@ -14,9 +14,14 @@
 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
+ end
+
+val add_obj: #status as 'status -> NUri.uri -> NCic.obj -> 'status
 val aliases_of: NUri.uri -> NReference.reference list
 val resolve: string -> NReference.reference list
 (* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *)
@@ -24,7 +29,7 @@ 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 =