]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicLibrary.ml
Initial implementation of statuses using objects in place of nested records.
[helm.git] / helm / software / components / ng_kernel / nCicLibrary.ml
index cc13dde6e306959c18ba48d0a64f4a992c1e7012..1cb3a118b40c44eae03ac7bd6b445c6f9ea02162 100644 (file)
@@ -23,7 +23,17 @@ let storage = ref [];;
 let aliases = ref [];;
 let cache = ref NUri.UriMap.empty;;
 
-let time_travel (sto,ali,cac) = storage := sto; aliases := ali; cache := cac;;
+class status =
+ object
+  val timestamp = (time0 : timestamp)
+  method timestamp = timestamp
+  method set_timestamp v = {< timestamp = v >}
+ end
+
+let time_travel status =
+ let sto,ali,cac = status#timestamp in
+  storage := sto; aliases := ali; cache := cac
+;;
 
 let path_of_baseuri baseuri =
  let uri = NUri.string_of_uri baseuri in
@@ -56,7 +66,7 @@ let serialize ~baseuri dump =
     Marshal.to_channel ch (magic,obj) [];
     close_out ch
   ) !storage;
- time_travel time0
+ time_travel (new status)
 ;;
 
 let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
@@ -139,7 +149,7 @@ let aliases_of uri =
   Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri)))
 ;;
 
-let add_obj u obj =
+let add_obj status u obj =
  storage := (u,obj)::!storage;
   let _,height,_,_,obj = obj in
   let references =
@@ -170,7 +180,7 @@ let add_obj u obj =
          ) il)
   in
   aliases := references @ !aliases;
-  !storage,!aliases,!cache
+  status#set_timestamp (!storage,!aliases,!cache)
 ;;
 
 let get_obj u =