helm/matita/matitaclean.ml

   1 module UM = UriManager;;
   2 module TA = TacticAst;;
   3
   4 let _ =
   5   Helm_registry.load_from "matita.conf.xml";
   6   Http_getter.init ();
   7   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner")
   8
   9 let main uri_to_remove = MatitacleanLib.clean_baseuris uri_to_remove
  10
  11 let usage () =
  12   prerr_endline "";
  13   prerr_endline "usage:";
  14   prerr_endline "\tmatitaclean all";
  15   prerr_endline "\tmatitaclean (uri|file)+";
  16   prerr_endline "";
  17   exit 1
  18
  19 let _ =
  20   if Array.length Sys.argv < 2 then usage ();
  21   if Sys.argv.(1) = "all" then
  22     begin
  23       MatitaDb.reset_owner_environment ();
  24       exit 0
  25     end
  26   let uri_to_remove =ref [] in
  27   (try
  28     for i = 1 to Array.length Sys.argv - 1 do
  29       let suri = Sys.argv.(i) in
  30       let uri =
  31         try
  32           UM.buri_of_uri (UM.uri_of_string suri)
  33         with
  34           UM.IllFormedUri _ -> MatitacleanLib.baseuri_of_file suri
  35       in
  36       uri_to_remove := uri :: !uri_to_remove
  37     done
  38   with
  39     Invalid_argument _ -> usage ());
  40   main !uri_to_remove
  41