+ debug_prerr "clean_baseuri will remove:";
+ if debug then
+ List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
+ List.iter
+ (fun buri ->
+ MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri))
+ (HExtlib.list_uniq (List.fast_sort Pervasives.compare
+ (List.map (UriManager.buri_of_uri) l)));
+ List.iter (MatitaSync.remove ~verbose) l;
+ cleaned_no := !cleaned_no + List.length l;
+ if !cleaned_no > 30 then
+ begin
+ cleaned_no := 0;
+ List.iter
+ (function table ->
+ ignore (HMysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
+ [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
+ MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
+ MetadataTypes.count_tbl()]
+ end
+
+let baseuri_of_file file =
+ let uri = ref None in
+ let ic = open_in file in
+ let istream = Ulexing.from_utf8_channel ic in
+ (try
+ while true do
+ try
+ let stm = GrafiteParser.parse_statement istream in
+ match MatitaMisc.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(Http_getter.resolve u)
+ with
+ | Http_getter_types.Unresolvable_URI _ ->
+ MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
+ | Http_getter_types.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
+ | Some uri -> uri
+ | None -> failwith ("No baseuri defined in " ^ file)
+
+let obj_file_of_script f =
+ if f = "coq.ma" then BuildTimeConf.coq_notation_script else
+ let baseuri = baseuri_of_file f in
+ MatitaMisc.obj_file_of_baseuri baseuri