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 -> ()
+ try
+ 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 -> ()
+ with
+ CicNotationParser.Parse_error _ as exn ->
+ prerr_endline ("Unable to parse: " ^ file);
+ prerr_endline (MatitaExcPp.to_string exn);
+ ()
done
with End_of_file -> close_in ic);
match !uri with
| [] -> uris
| l -> let uris, next = close_uri_list l in fix uris next @ uris
+let cleaned_no = ref 0;;
+
let clean_baseuris ?(verbose=true) buris =
Hashtbl.clear cache_of_processed_baseuri;
let buris = List.map HGM.strip_trailing_slash buris in
debug_prerr "clean_baseuri will remove:";
if debug then
List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
- List.iter (MatitaSync.remove ~verbose) l
+ List.iter (MatitaSync.remove ~verbose) l;
+ cleaned_no := !cleaned_no + List.length l;
+ if !cleaned_no > 30 then
+ List.iter
+ (function table ->
+ ignore (Mysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
+ [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 ^ "/") = []