From 63722506a5e378f3e05b46612cb91c132d994082 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 5 Jul 2005 08:45:16 +0000 Subject: [PATCH] * safe_remove exported and moved to MatitaMisc * safe_remove used to remove the files from disk --- helm/matita/matitaDb.ml | 2 +- helm/matita/matitaMisc.ml | 2 ++ helm/matita/matitaMisc.mli | 3 +++ helm/matita/matitaSync.ml | 6 ++---- 4 files changed, 8 insertions(+), 5 deletions(-) diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml index 089aab157..0c10a81e8 100644 --- a/helm/matita/matitaDb.ml +++ b/helm/matita/matitaDb.ml @@ -66,7 +66,7 @@ let clean_owner_environment () = (fun uri -> let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in List.iter - (fun suffix -> Http_getter_storage.remove (uri ^ suffix ^ ".xml.gz")) + (fun suffix -> MatitaMisc.safe_remove (uri ^ suffix ^ ".xml.gz")) [""; ".body"; ".types"]) owned_uris; List.iter (fun statement -> diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 1ea4e7e92..81f185ae8 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -26,6 +26,8 @@ open Printf open MatitaTypes +let safe_remove fname = if Sys.file_exists fname then Sys.remove fname + let is_dir fname = try (Unix.stat fname).Unix.st_kind = Unix.S_DIR diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index c2cba5903..c5ff2ace6 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -23,6 +23,9 @@ * http://helm.cs.unibo.it/ *) +(** removes a file if it exists *) +val safe_remove: string -> unit + val is_dir: string -> bool (** @return true if file is a directory *) val is_regular: string -> bool (** @return true if file is a regular file *) diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 374b47870..23e3b048f 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -178,15 +178,13 @@ let delta_status status1 status2 = 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 @@ -240,7 +238,7 @@ let remove uri = (fun uri -> (try MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri); - safe_remove (Http_getter.resolve' uri) + MatitaMisc.safe_remove (Http_getter.resolve' uri) with Http_getter_types.Key_not_found _ -> ()); remove_coercion uri; ignore (MatitaDb.remove_uri uri)) -- 2.39.2