+let require0 ~baseuri = require_path (path_of_baseuri baseuri);;
+
+let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
+
+
+type timestamp =
+ [ `Obj of NUri.uri * NCic.obj
+ | `Constr of bool * NCic.universe * NCic.universe] list *
+ (NUri.uri * string * NReference.reference) list *
+ NCic.obj NUri.UriMap.t *
+ NUri.uri list
+;;
+
+let time0 = [],[],NUri.UriMap.empty,[];;
+let storage = ref [];;
+let local_aliases = ref [];;
+let cache = ref NUri.UriMap.empty;;
+let includes = ref [];;
+
+let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
+ let global_aliases = ref [] in
+ let rev_includes_map = ref NUri.UriMap.empty in
+ let store_db () =
+ let ch = open_out (db_path ()) in
+ Marshal.to_channel ch (magic,(!global_aliases,!rev_includes_map)) [];
+ close_out ch in
+ let load_db () =
+ HExtlib.mkdir (Helm_registry.get "matita.basedir");
+ try
+ let ga,im = require_path (db_path ()) in
+ let ga =
+ List.map
+ (fun (uri,name,NReference.Ref (uri2,spec)) ->
+ refresh_uri uri,name,NReference.reference_of_spec (refresh_uri uri2) spec
+ ) ga in
+ let im =
+ NUri.UriMap.fold
+ (fun u l im -> NUri.UriMap.add (refresh_uri u) (List.map refresh_uri l) im
+ ) im NUri.UriMap.empty
+ in
+ global_aliases := ga;
+ rev_includes_map := im
+ with
+ Sys_error _ -> () in
+ let get_deps u =
+ let get_deps_one_step u =
+ try NUri.UriMap.find u !rev_includes_map with Not_found -> [] in
+ let rec aux res =
+ function
+ [] -> res
+ | he::tl ->
+ if List.mem he res then
+ aux res tl
+ else
+ aux (he::res) (get_deps_one_step he @ tl)
+ in
+ aux [] [u] in
+ let remove_deps u =
+ rev_includes_map := NUri.UriMap.remove u !rev_includes_map;
+ rev_includes_map :=
+ NUri.UriMap.map
+ (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !rev_includes_map;
+ store_db ()
+ in
+ load_db,
+ (fun ga -> global_aliases := ga; store_db ()),
+ (fun () -> !global_aliases),
+ (fun u l ->
+ rev_includes_map := NUri.UriMap.add u (l @ get_deps u) !rev_includes_map;
+ store_db ()),
+ get_deps,
+ remove_deps
+;;
+
+let init = load_db;;
+
+
+class status =
+ object
+ val timestamp = (time0 : timestamp)
+ method timestamp = timestamp
+ method set_timestamp v = {< timestamp = v >}
+ method set_library_status
+ : 'status. < timestamp : timestamp; .. > as 'status -> 'self
+ = fun o -> {< timestamp = o#timestamp >}
+ end
+
+let time_travel status =
+ let sto,ali,cac,inc = status#timestamp in
+ let diff_len = List.length !storage - List.length sto in
+ let to_be_deleted,_ = HExtlib.split_nth diff_len !storage in
+ if List.length to_be_deleted > 0 then
+ NCicEnvironment.invalidate_item (HExtlib.list_last to_be_deleted);
+ storage := sto; local_aliases := ali; cache := cac; includes := inc
+;;
+