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")
(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);
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:";
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
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