From d7c24dbca4f5e2baef606669db70cc640c02d38d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 26 Sep 2005 12:32:26 +0000
Subject: [PATCH] MatitacleanLib.remove_baseuris will remove empty directories.

---
 helm/matita/matita.txt        |  4 ++--
 helm/matita/matitaMisc.ml     | 22 ++++++++++++++++++++++
 helm/matita/matitaMisc.mli    |  6 ++++++
 helm/matita/matitaSync.ml     |  4 +++-
 helm/matita/matitacleanLib.ml |  4 ++--
 5 files changed, 35 insertions(+), 5 deletions(-)

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 11968e849..daba1943c 100644
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -91,8 +91,6 @@ TODO
   - default equality e famiglia non e' undo-aware
   - nuovo pretty-printer testuale: non stampa usando la notazione
     (e.g. guardare output di matitac)
-  - matitaclean (e famiglia) non cancellano le directory vuote
-    (e per giunta il cicbrowser le mostra :-)
   - fattorizzare codice fra MatitaEngine e DisambiguatePp (dove, fra l'altro,
     ora io (=CSC) ho messo anche un parser!!!)
   - bug "Warn:  baseuri cic:/matita/higher_order_defs/ordering is not empty"
@@ -108,6 +106,8 @@ TODO
   DEMONI E ALTRO
 
 DONE
+- matitaclean (e famiglia) non cancellano le directory vuote
+  (e per giunta il cicbrowser le mostra :-) -> Gares
 - missing feature unification: applicazione di teoremi (~A) quando il goal
   e' False o di teoremi $symmetric R P$ quando il goal e' $P(x,y)$.
   Fare un passo di delta[-beta?][-iota-etc.] quando da una parte c'e' una
diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 9c0c7db33..e86e4b9a0 100644
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -80,6 +80,28 @@ let is_empty buri =
 
 let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
 
+let is_dir_empty d =
+  try 
+    let od = Unix.opendir d in
+    try 
+      ignore (Unix.readdir od);
+      ignore (Unix.readdir od);
+      ignore (Unix.readdir od);
+      Unix.closedir od;
+      false
+    with End_of_file -> 
+      Unix.closedir od;
+      true
+  with Unix.Unix_error _ -> true
+
+let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> ()
+
+let rec rmdir_descend d = 
+  if is_dir_empty d then
+    begin
+      safe_rmdir d;
+      rmdir_descend (Filename.dirname d)
+    end
 
 let absolute_path file =
   if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli
index bf51c64e9..0c2063095 100644
--- a/helm/matita/matitaMisc.mli
+++ b/helm/matita/matitaMisc.mli
@@ -33,6 +33,12 @@ val is_empty: string -> bool
 
 (** removes a file if it exists *)
 val safe_remove: string -> unit
+(** removes a dir if it exists and is empty *)
+val safe_rmdir: string -> unit 
+(** checks if the dir is empty *)
+val is_dir_empty: string -> bool
+(** removes a directory and recursively the father (if empty) *)
+val rmdir_descend: string -> unit
 
 val absolute_path: string -> string 
 
diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 3383ee312..f2c9d6e33 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -306,7 +306,9 @@ let remove ?(verbose=false) uri =
             MatitaLog.debug ("Removing: " ^ baseuri ^ "/*");
             last_baseuri := baseuri
            end;
-        MatitaMisc.safe_remove (Http_getter.resolve' uri)
+           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);
diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml
index a263a526f..51268acef 100644
--- a/helm/matita/matitacleanLib.ml
+++ b/helm/matita/matitacleanLib.ml
@@ -143,8 +143,8 @@ let clean_baseuris ?(verbose=true) buris =
     List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; 
   Hashtbl.iter
    (fun buri _ ->
-     MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri)
-   ) cache_of_processed_baseuri;
+     MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri)) 
+   cache_of_processed_baseuri;
   List.iter (MatitaSync.remove ~verbose) l;
   cleaned_no := !cleaned_no + List.length l;
   if !cleaned_no > 30 then
-- 
2.39.2