From: Claudio Sacerdoti Coen Date: Fri, 19 Jun 2009 14:59:35 +0000 (+0000) Subject: Bug fixed: refreshing of uris for the db. X-Git-Tag: make_still_working~3834 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f2d96fcafce09d26d483fa18a9e6e36124a462c9;p=helm.git Bug fixed: refreshing of uris for the db. --- diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index a36b70bf4..0519e4146 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -15,6 +15,22 @@ exception LibraryOutOfSync of string Lazy.t let magic = 0;; +let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);; + +let rec refresh_uri_in_term = + function + NCic.Const (NReference.Ref (u,spec)) -> + NCic.Const (NReference.reference_of_spec (refresh_uri u) spec) + | t -> NCicUtils.map (fun _ _ -> ()) () (fun _ -> refresh_uri_in_term) t +;; + +let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) = + assert (metasenv = []); + assert (subst = []); + uri,height,metasenv,subst, + NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind +;; + let path_of_baseuri ?(no_suffix=false) baseuri = let uri = NUri.string_of_uri baseuri in let path = String.sub uri 4 (String.length uri - 4) in @@ -49,6 +65,7 @@ type timestamp = 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 () = @@ -62,7 +79,14 @@ let set_global_aliases,get_global_aliases = let init () = try - set_global_aliases (require_path (db_path ())) + let global_aliases = require_path (db_path ()) in + let global_aliases = + List.map + (fun (uri,name,NReference.Ref (uri2,spec)) -> + refresh_uri uri,name,NReference.reference_of_spec (refresh_uri uri2) spec + ) global_aliases + in + set_global_aliases global_aliases with Sys_error _ -> () ;; @@ -98,22 +122,6 @@ let serialize ~baseuri dump = time_travel (new status) ;; -let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);; - -let rec refresh_uri_in_term = - function - NCic.Const (NReference.Ref (u,spec)) -> - NCic.Const (NReference.reference_of_spec (refresh_uri u) spec) - | t -> NCicUtils.map (fun _ _ -> ()) () (fun _ -> refresh_uri_in_term) t -;; - -let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) = - assert (metasenv = []); - assert (subst = []); - uri,height,metasenv,subst, - NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind -;; - module type Serializer = sig type status