X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibraryClean.ml;h=a544991e85b109e3df0f74f68b27efaf04c612e5;hb=d265b4b4fac92685c29f89887c1083a494bae6e5;hp=6f72ff495b77edf2389397863bf56bd7de3778b3;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/library/libraryClean.ml b/components/library/libraryClean.ml
index 6f72ff495..a544991e8 100644
--- a/components/library/libraryClean.ml
+++ b/components/library/libraryClean.ml
@@ -147,7 +147,7 @@ let moo_root_dir = lazy (
   String.sub url 7 (String.length url - 7)  (* remove heading "file:///" *)
 )
 
-let close_nodb ~basedir buris =
+let close_nodb buris =
   let rev_deps = Hashtbl.create 97 in
   let all_metadata =
     HExtlib.find ~test:(fun name -> Filename.check_suffix name ".metadata")
@@ -157,6 +157,8 @@ let close_nodb ~basedir buris =
     (fun path -> 
       let metadata = LibraryNoDb.load_metadata ~fname:path in
       let baseuri_of_current_metadata =
+       prerr_endline "ERROR, add to the getter reverse lookup";
+       let basedir = "/fake" in
        let dirname = Filename.dirname path in
        let basedirlen = String.length basedir in
         assert (String.sub dirname 0 basedirlen = basedir);
@@ -190,7 +192,7 @@ let close_nodb ~basedir buris =
   in
   objects_to_remove
 
-let clean_baseuris ?(verbose=true) ~basedir buris =
+let clean_baseuris ?(verbose=true) buris =
   Hashtbl.clear cache_of_processed_baseuri;
   let buris = List.map Http_getter_misc.strip_trailing_slash buris in
   debug_prerr "clean_baseuris called on:";
@@ -198,7 +200,7 @@ let clean_baseuris ?(verbose=true) ~basedir buris =
     List.iter debug_prerr buris; 
   let l = 
     if Helm_registry.get_bool "db.nodb" then
-      close_nodb ~basedir buris
+      close_nodb buris
     else
       close_db [] buris 
   in
@@ -208,19 +210,32 @@ let clean_baseuris ?(verbose=true) ~basedir buris =
   if debug then
     List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; 
   List.iter
-   (fun buri ->
-     HExtlib.safe_remove (LibraryMisc.obj_file_of_baseuri basedir buri);
-     HExtlib.safe_remove (LibraryMisc.metadata_file_of_baseuri basedir buri);
-     HExtlib.safe_remove (LibraryMisc.lexicon_file_of_baseuri basedir buri))
+   (fun baseuri ->
+     try 
+      let obj_file =
+       LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri
+      in
+       HExtlib.safe_remove obj_file ;
+       HExtlib.safe_remove 
+         (LibraryMisc.metadata_file_of_baseuri 
+           ~must_exist:false ~writable:true ~baseuri) ;
+       HExtlib.safe_remove 
+         (LibraryMisc.lexicon_file_of_baseuri 
+           ~must_exist:false ~writable:true ~baseuri) ;
+       HExtlib.rmdir_descend (Filename.chop_extension obj_file)
+     with Http_getter_types.Key_not_found _ -> ())
    (HExtlib.list_uniq (List.fast_sort Pervasives.compare
-     (List.map (UriManager.buri_of_uri) l)));
+     (List.map (UriManager.buri_of_uri) l @ buris)));
   List.iter
    (let last_baseuri = ref "" in
     fun uri ->
      let buri = UriManager.buri_of_uri uri in
      if buri <> !last_baseuri then
       begin
-       HLog.message ("Removing: " ^ buri ^ "/*");
+        if Helm_registry.get_bool "matita.bench" then
+            (print_endline ("matitaclean " ^ buri ^ "/");flush stdout)
+          else 
+            HLog.message ("Removing: " ^ buri ^ "/*");
        last_baseuri := buri
       end;
      LibrarySync.remove_obj uri