MatitacleanLib.remove_baseuris will remove empty directories.

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 11968e849c7a48f5067c08af6b58f1817b7a7b8c..daba1943c8faed6dee601b3ef693a1e704e2dc00 100644 (file)
--- 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 9c0c7db33338f6a40e8bc2267d96d43324027c81..e86e4b9a051e33ecfc81ab671b25cc7bd4359c48 100644 (file)
--- 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 bf51c64e9c8d0d795f3ace322c57d6e19ac7aa35..0c2063095d7dc9ab29a7fb0d360081cc1955c0e7 100644 (file)
--- 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 3383ee312e0df59e3fd0f9195eb0f1591184eaf2..f2c9d6e336858c9d236524a5752c81ce1f00ce09 100644 (file)
--- 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 a263a526fd7e05a65855b3413a8eecef3818b630..51268acef0c8084216a7107346308b23813f3416 100644 (file)
--- 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