helm/matita/matitaclean.ml

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