+module HGT = Http_getter_types;;
+module HG = Http_getter;;
+module UM = UriManager;;
+
+let _ =
+ Helm_registry.load_from "matita.conf.xml";
+ HG.init ();
+ MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner")
+
+let clean_all () =
+ MatitaDb.clean_owner_environment ();
+ MatitaDb.create_owner_environment ();
+ exit 0
+
+let dbd = MatitaDb.instance ()
+
+let one_step_depend suri =
+ let dbg_q =
+ let suri = Mysql.escape suri in
+ (**** FIX FIX FIX ***)
+ (****** let obj_tbl = MetadataTypes.obj_tbl () in ******)
+ let obj_tbl = MetadataTypes.library_obj_tbl in
+ (**** FIX FIX FIX ***)
+ Printf.sprintf
+ "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl suri
+ in
+ try
+ let rc = Mysql.exec dbd dbg_q in
+ let l = ref [] in
+ Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
+ let l = List.sort Pervasives.compare !l in
+ MatitaMisc.list_uniq l
+ with
+ exn -> raise exn (* no errors should be accepted *)
+
+let cache_of_processed_baseuri = Hashtbl.create 1024
+
+let close_uri_list uri_to_remove =
+ (* to remove an uri you have to remove the whole script *)
+ let buri_to_remove =
+ MatitaMisc.list_uniq
+ (List.fast_sort Pervasives.compare
+ (List.map UM.buri_of_uri uri_to_remove))
+ in
+ (* cleand the already visided baseuris *)
+ let buri_to_remove =
+ List.filter
+ (fun buri ->
+ if Hashtbl.mem cache_of_processed_baseuri buri then false
+ else true)
+ buri_to_remove
+ in
+ List.iter
+ (fun buri -> Hashtbl.add cache_of_processed_baseuri buri true)
+ buri_to_remove;
+ (* now calculate the list of objects that belong to these baseuris *)
+ let uri_to_remove =
+ List.fold_left
+ (fun acc buri ->
+ let inhabitants = HG.ls buri in
+ let inhabitants = List.filter
+ (function HGT.Ls_object _ -> true | _ -> false)
+ inhabitants
+ in
+ let inhabitants = List.map
+ (function
+ | HGT.Ls_object e -> UM.uri_of_string (buri ^ "/" ^ e.HGT.uri)
+ | _ -> assert false)
+ inhabitants
+ in
+ inhabitants @ acc)
+ [] buri_to_remove
+ in
+ (* now we want the list of all uri that depend on them *)
+ let depend =
+ List.fold_left
+ (fun acc u -> one_step_depend (UM.string_of_uri u) @ acc) [] uri_to_remove
+ in
+ let depend =
+ MatitaMisc.list_uniq
+ (List.fast_sort Pervasives.compare depend)
+ in
+ let depend = List.map UM.uri_of_string depend in
+ uri_to_remove, depend
+
+let main uri_to_remove =
+ let rec fix uris next =
+ match next with
+ | [] -> uris
+ | l -> let uris, next = close_uri_list l in fix uris next @ uris
+ in
+ MatitaMisc.list_uniq
+ (List.fast_sort Pervasives.compare (fix [] uri_to_remove))
+
+let usage () =
+ prerr_endline "";
+ prerr_endline "usage:";
+ prerr_endline "\tmatitaclean all";
+ prerr_endline "\tmatitaclean dry uris...";
+ prerr_endline "\tmatitaclean uris...";
+ prerr_endline "";
+ exit 1
+
+let _ =
+ at_exit
+ (fun () ->
+ Http_getter_logger.log "Sync map tree to disk...";
+ Http_getter.sync_dump_file ();
+ print_endline "\nThanks for using Matita!\n");
+ if Array.length Sys.argv < 2 then usage ();
+ if Sys.argv.(1) = "all" then clean_all ();
+ let start, dry =
+ if Sys.argv.(1) = "dry" then 2, true else 1, false
+ in
+ let uri_to_remove =ref [] in
+ try
+ for i = start to Array.length Sys.argv - 1 do
+ let suri = Sys.argv.(i) in
+ let uri = UM.uri_of_string suri in
+ uri_to_remove := uri :: !uri_to_remove
+ done
+ with
+ Invalid_argument _ -> usage ();
+ let l = main !uri_to_remove in
+ if dry then
+ begin
+ List.iter (fun x -> let u = UM.string_of_uri x in prerr_endline u) l;
+ exit 0
+ end
+ else
+ List.iter
+ (fun u ->
+ prerr_endline ("Removing " ^ UM.string_of_uri u);
+ MatitaSync.remove u)
+ l
+