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 >}
+ method set_library_status (o : status) = {< timestamp = o#timestamp >}
+ 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
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);;
sig
type status
type obj
- val register: string -> ('a -> status -> status) -> ('a -> obj)
+ val register:
+ string ->
+ ('a -> 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
already_registered := tag :: !already_registered;
require1 :=
(fun (tag',data) as x ->
- if tag=tag' then require (Obj.magic data) else !require1 x);
+ if tag=tag' then
+ require (Obj.magic data) ~refresh_uri_in_term
+ else
+ !require1 x);
(fun x -> tag,Obj.repr x)
let serialize = serialize
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 =
) il)
in
aliases := references @ !aliases;
- !storage,!aliases,!cache
+ status#set_timestamp (!storage,!aliases,!cache)
;;
let get_obj u =