exception LibraryOutOfSync of string Lazy.t
-type timestamp =
- (NUri.uri * NCic.obj) list *
- (NUri.uri * string * NReference.reference) list *
- NCic.obj NUri.UriMap.t;;
-
-let time0 = [],[],NUri.UriMap.empty;;
-let storage = ref [];;
-let local_aliases = ref [];;
-let global_aliases = ref [];;
-let cache = ref NUri.UriMap.empty;;
-
-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 = status#timestamp in
- storage := sto; local_aliases := ali; cache := cac
-;;
+let magic = 0;;
let path_of_baseuri ?(no_suffix=false) baseuri =
let uri = NUri.string_of_uri baseuri in
path ^ ".ng"
;;
-let magic = 0;;
-
let require_path path =
let ch = open_in path in
let mmagic,dump = Marshal.from_channel ch in
let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
+type timestamp =
+ (NUri.uri * NCic.obj) list *
+ (NUri.uri * string * NReference.reference) list *
+ NCic.obj NUri.UriMap.t;;
+
+let time0 = [],[],NUri.UriMap.empty;;
+let storage = ref [];;
+let local_aliases = ref [];;
+let set_global_aliases,get_global_aliases =
+ let global_aliases = ref [] in
+ let store_db () =
+ let ch = open_out (db_path ()) in
+ Marshal.to_channel ch (magic,!global_aliases) [];
+ close_out ch;
+ in
+ (fun ga -> global_aliases := ga; store_db ()),
+ (fun () -> !global_aliases)
+;;
+
let init () =
try
- global_aliases := require_path (db_path ())
+ set_global_aliases (require_path (db_path ()))
with
Sys_error _ -> ()
;;
+let cache = ref NUri.UriMap.empty;;
+
+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 = status#timestamp in
+ storage := sto; local_aliases := ali; cache := cac
+;;
+
let serialize ~baseuri dump =
let ch = open_out (path_of_baseuri baseuri) in
Marshal.to_channel ch (magic,dump) [];
Marshal.to_channel ch (magic,obj) [];
close_out ch
) !storage;
- global_aliases := !local_aliases @ !global_aliases;
- let ch = open_out (db_path ()) in
- Marshal.to_channel ch (magic,!global_aliases) [];
- close_out ch;
+ set_global_aliases (!local_aliases @ get_global_aliases ());
time_travel (new status)
;;
let names = List.map (fun name -> basepath ^ "/" ^ name) (aux []) in
Unix.closedir od;
List.iter Unix.unlink names;
- HExtlib.rmdir_descend basepath
+ HExtlib.rmdir_descend basepath;
+ set_global_aliases
+ (List.filter
+ (fun (_,_,NReference.Ref (nuri,_)) ->
+ Filename.dirname (NUri.string_of_uri nuri) <> NUri.string_of_uri baseuri
+ ) (get_global_aliases ()))
with
Unix.Unix_error _ -> () (* raised by Unix.opendir, we hope :-) *)
;;
try
HExtlib.filter_map
(fun (_,name',nref) -> if name'=name then Some nref else None)
- (!local_aliases @ !global_aliases)
+ (!local_aliases @ get_global_aliases ())
with
Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name))
;;