* safe_remove exported and moved to MatitaMisc

* safe_remove used to remove the files from disk

diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml
index 089aab157abc72b800018d84372fa7d6a6a98aeb..0c10a81e855463ce12ca15b3dac8e407854dc0ce 100644 (file)
--- 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 1ea4e7e9228c52ffca09fcaa81b4a66e0b5be968..81f185ae83ef4e590e0409e603df1e851591e3ad 100644 (file)
--- 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 c2cba5903192744d61ba9ec7264d1a297ef84e5b..c5ff2ace68046907b6524b252d0b289d6d06c781 100644 (file)
--- 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 374b47870324175c04295ba1e8d749589d2def4c..23e3b048f45bd015a184d2b6273b9cd257c1406e 100644 (file)
--- 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))