module UM = UriManager;;
module TA = GrafiteAst;;
-let baseuri_of_baseuri_decl st =
- match st with
- | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
- Some buri
- | _ -> None
-
let cache_of_processed_baseuri = Hashtbl.create 1024
let one_step_depend suri =
in
uri_to_remove, depend
-let baseuri_of_file file =
- let uri = ref None in
- let ic = open_in file in
- let istream = Stream.of_channel ic in
- (try
- while true do
- let stm = GrafiteParser.parse_statement istream in
- match baseuri_of_baseuri_decl stm with
- | Some buri ->
- let u = MatitaMisc.strip_trailing_slash buri in
- if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
- MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
- (try
- ignore(HG.resolve u)
- with
- | HGT.Unresolvable_URI _ ->
- MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
- | HGT.Key_not_found _ -> ());
- uri := Some u;
- raise End_of_file
- | None -> ()
- done
- with End_of_file -> close_in ic);
- match !uri with
- | Some uri -> uri
- | None -> failwith ("No baseuri defined in " ^ file)
-
-let rec fix uris next =
+let rec close uris next =
match next with
| [] -> uris
- | l -> let uris, next = close_uri_list l in fix uris next @ uris
+ | l -> let uris, next = close_uri_list l in close uris next @ uris
let cleaned_no = ref 0;;
debug_prerr "clean_baseuris called on:";
if debug then
List.iter debug_prerr buris;
- let l = fix [] buris in
+ let l = close [] buris in
let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in
let l = List.map UriManager.uri_of_string l in
debug_prerr "clean_baseuri will remove:";
if debug then
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;
List.iter (MatitaSync.remove ~verbose) l;
cleaned_no := !cleaned_no + List.length l;
if !cleaned_no > 30 then
[MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
MetadataTypes.count_tbl()]
-
-let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = []
-