X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=f2c9d6e336858c9d236524a5752c81ce1f00ce09;hb=86af949158e013178557c7fec7662ac06fae753c;hp=3351725db23b5be93a1274a3ed0cf26ab6746679;hpb=675c9cf70d8537d70675b5520ca708fe75c67aed;p=helm.git diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 3351725db..f2c9d6e33 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -43,8 +43,8 @@ let alias_diff ~from status = status.aliases [] let alias_diff = - let profiler = CicUtil.profile "alias_diff (conteggiato anche in include)" in - fun ~from status -> profiler.CicUtil.profile (alias_diff ~from) status + let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in + fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status let set_proof_aliases status new_aliases = let aliases = @@ -63,11 +63,6 @@ let set_proof_aliases status new_aliases = (DisambiguatePp.commands_of_domain_and_codomain_items_list new_aliases) new_status -let compute_diff_and_set_proof_aliases status aliases = - let new_status = { status with aliases = aliases } in - let diff = alias_diff ~from:status new_status in - set_proof_aliases status diff - (** given a uri and a type list (the contructors types) builds a list of pairs * (name,uri) that is used to generate authomatic aliases **) let extract_alias types uri = @@ -111,6 +106,7 @@ let paths_and_uris_of_obj uri status = let basedir = get_string_option status "basedir" ^ "/xml" in let innertypesuri = UriManager.innertypesuri_of_uri uri in let bodyuri = UriManager.bodyuri_of_uri uri in + let univgraphuri = UriManager.univgraphuri_of_uri uri in let innertypesfilename = Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in let innertypespath = basedir ^ "/" ^ innertypesfilename in @@ -120,12 +116,16 @@ let paths_and_uris_of_obj uri status = let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") "" (UriManager.string_of_uri uri) ^ ".body.xml.gz" in let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in - xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri + let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") "" + (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in + let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in + xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, + xmlunivgraphpath, univgraphuri -let save_object_to_disk status uri obj = +let save_object_to_disk status uri obj ugraph univlist = let ensure_path_exists path = let dir = Filename.dirname path in - MatitaMisc.mkdir dir + HExtlib.mkdir dir in (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *) let annobj = Cic2acic.plain_acic_object_of_cic_object obj in @@ -134,17 +134,19 @@ let save_object_to_disk status uri obj = Cic2Xml.print_object uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj in - let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri = + let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, + xmlunivgraphpath, univgraphuri = paths_and_uris_of_obj uri status in let path_scheme_of path = "file://" ^ path in - List.iter MatitaMisc.mkdir - (List.map Filename.dirname [innertypespath; xmlpath]); + List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]); (* now write to disk *) ensure_path_exists xmlpath; - Xml.pp ~gzip:true xml (Some xmlpath) ; + Xml.pp ~gzip:true xml (Some xmlpath); + CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist; (* we return a list of uri,path we registered/created *) (uri,xmlpath) :: + (univgraphuri,xmlunivgraphpath) :: (* now the optional body, both write and register *) (match bodyxml,bodyuri with None,None -> [] @@ -155,18 +157,13 @@ let save_object_to_disk status uri obj = | _-> assert false) let typecheck_obj = - let profiler = CicUtil.profile "add_obj.typecheck_obj" in - fun uri obj -> profiler.CicUtil.profile (CicTypeChecker.typecheck_obj uri) obj + let profiler = HExtlib.profile "add_obj.typecheck_obj" in + fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj let index_obj = - let profiler = CicUtil.profile "add_obj.index_obj" in + let profiler = HExtlib.profile "add_obj.index_obj" in fun ~dbd ~uri -> - profiler.CicUtil.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri - -let save_object_to_disk = - let profiler = CicUtil.profile "add_obj.save_object_to_disk" in - fun status uri obj -> - profiler.CicUtil.profile (save_object_to_disk status uri) obj + profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri let add_obj uri obj status = let dbd = MatitaDb.instance () in @@ -175,10 +172,12 @@ let add_obj uri obj status = command_error (sprintf "%s already defined" suri) else begin typecheck_obj uri obj; (* 1 *) + let _, ugraph, univlist = + CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in try index_obj ~dbd ~uri; (* 2 must be in the env *) try - let new_stuff = save_object_to_disk status uri obj in (* 3 *) + let new_stuff=save_object_to_disk status uri obj ugraph univlist in(*3*) try MatitaLog.message (sprintf "%s defined" suri); let status = add_aliases_for_object status suri obj in @@ -192,12 +191,12 @@ let add_obj uri obj status = raise exc with exc -> CicEnvironment.remove_obj uri; (* -1 *) - raise exc + raise exc end let add_obj = - let profiler = CicUtil.profile "add_obj" in - fun uri obj status -> profiler.CicUtil.profile (add_obj uri obj) status + let profiler = HExtlib.profile "add_obj" in + fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status module OrderedUri = struct @@ -281,12 +280,15 @@ let time_travel ~present ~past = List.iter MatitaLog.debug l2 *) -let remove ~verbose uri = +let last_baseuri = ref "" + +let remove ?(verbose=false) uri = let derived_uris_of_uri uri = UriManager.innertypesuri_of_uri uri :: + UriManager.univgraphuri_of_uri uri :: (match UriManager.bodyuri_of_uri uri with | None -> [] - | Some u -> [u]) + | Some u -> [u]) in let to_remove = uri :: @@ -296,9 +298,17 @@ let remove ~verbose uri = List.iter (fun uri -> (try + (* WARNING: non reentrant debugging code *) if verbose then - MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri); - MatitaMisc.safe_remove (Http_getter.resolve' uri) + let baseuri = UriManager.buri_of_uri uri in + if !last_baseuri <> baseuri then + begin + MatitaLog.debug ("Removing: " ^ baseuri ^ "/*"); + last_baseuri := baseuri + end; + let file = Http_getter.resolve' uri in + MatitaMisc.safe_remove file; + MatitaMisc.rmdir_descend (Filename.dirname file) with Http_getter_types.Key_not_found _ -> ()); remove_coercion uri; ignore (MatitaDb.remove_uri uri);