if not (Map.mem domain_item from.aliases) then
Map.add domain_item codomain_item acc
else
- acc)
+ begin
+ try
+ let description1 = fst(Map.find domain_item from.aliases) in
+ let description2 = fst(Map.find domain_item status.aliases) in
+ if description1 <> description2 then
+ Map.add domain_item codomain_item acc
+ else
+ acc
+ with Not_found -> acc
+ end)
status.aliases Map.empty
let set_proof_aliases status aliases =
| Cic.CurrentProof _ -> assert false
let paths_and_uris_of_obj uri status =
- let basedir = get_string_option status "basedir" in
+ 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 innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
let remove_coercion uri =
CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)
-let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
-
let time_travel ~present ~past =
let list_of_objs_to_remove = List.rev (delta_status past present) in
(* List.rev is just for the debugging code, which otherwise may list both
* something.ind and something.ind#xpointer ... (ask Enrico :-) *)
let debug_list = ref [] in
List.iter (fun (uri,p) ->
- safe_remove p;
+ MatitaMisc.safe_remove p;
remove_coercion uri;
(try
CicEnvironment.remove_obj uri
MatitaLog.debug "l2:";
List.iter MatitaLog.debug l2
-let remove uri =
+let remove ~verbose uri =
let derived_uris_of_uri uri =
UriManager.innertypesuri_of_uri uri ::
(match UriManager.bodyuri_of_uri uri with
List.iter
(fun uri ->
(try
- MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri);
- safe_remove (Http_getter.resolve' uri)
+ if verbose then
+ MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri);
+ MatitaMisc.safe_remove (Http_getter.resolve' uri)
with Http_getter_types.Key_not_found _ -> ());
remove_coercion uri;
ignore (MatitaDb.remove_uri uri))
to_remove
-