1 module HGT = Http_getter_types;;
2 module HG = Http_getter;;
3 module UM = UriManager;;
4 module TA = TacticAst;;
7 Helm_registry.load_from "matita.conf.xml";
9 MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner")
12 MatitaDb.clean_owner_environment ();
13 MatitaDb.create_owner_environment ();
16 let dbd = MatitaDb.instance ()
17 let cache_of_processed_baseuri = Hashtbl.create 1024
19 let one_step_depend suri =
22 UM.buri_of_uri (UM.uri_of_string suri)
23 with UM.IllFormedUri _ -> suri
25 if Hashtbl.mem cache_of_processed_baseuri buri then
29 Hashtbl.add cache_of_processed_baseuri buri true;
31 let buri = buri ^ "/" in
32 let buri = Mysql.escape buri in
33 let obj_tbl = MetadataTypes.obj_tbl () in
35 "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
38 let rc = Mysql.exec dbd query in
40 Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l:=a:: !l);
41 let l = List.sort Pervasives.compare !l in
42 MatitaMisc.list_uniq l
44 exn -> raise exn (* no errors should be accepted *)
48 let safe_buri_of_suri suri =
50 UM.buri_of_uri (UM.uri_of_string suri)
52 UM.IllFormedUri _ -> suri
54 let close_uri_list uri_to_remove =
55 (* to remove an uri you have to remove the whole script *)
58 (List.fast_sort Pervasives.compare
59 (List.map safe_buri_of_suri uri_to_remove))
61 (* cleand the already visided baseuris *)
65 if Hashtbl.mem cache_of_processed_baseuri buri then false
69 (* now calculate the list of objects that belong to these baseuris *)
73 let inhabitants = HG.ls buri in
74 let inhabitants = List.filter
75 (function HGT.Ls_object _ -> true | _ -> false)
78 let inhabitants = List.map
80 | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri
87 (* now we want the list of all uri that depend on them *)
90 (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
94 (List.fast_sort Pervasives.compare depend)
98 let buri_of_file file =
99 let ic = open_in file in
100 let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in
105 | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
106 uri := MatitaMisc.strip_trailing_slash buri
111 let main uri_to_remove =
112 let rec fix uris next =
115 | l -> let uris, next = close_uri_list l in fix uris next @ uris
118 (List.fast_sort Pervasives.compare (fix [] uri_to_remove))
122 prerr_endline "usage:";
123 prerr_endline "\tmatitaclean all";
124 prerr_endline "\tmatitaclean dry (uri|file)+";
125 prerr_endline "\tmatitaclean (uri|file)+";
132 Http_getter_logger.log "Sync map tree to disk...";
133 Http_getter.sync_dump_file ();
134 print_endline "\nThanks for using Matita!\n");
135 if Array.length Sys.argv < 2 then usage ();
136 if Sys.argv.(1) = "all" then clean_all ();
138 if Sys.argv.(1) = "dry" then 2, true else 1, false
140 let uri_to_remove =ref [] in
142 for i = start to Array.length Sys.argv - 1 do
143 let suri = Sys.argv.(i) in
146 UM.buri_of_uri (UM.uri_of_string suri)
148 UM.IllFormedUri _ -> buri_of_file suri
150 uri_to_remove := uri :: !uri_to_remove
153 Invalid_argument _ -> usage ());
154 let l = main !uri_to_remove in
157 List.iter prerr_endline l;
163 prerr_endline ("Removing " ^ u);
165 MatitaSync.remove (UM.uri_of_string u)
166 with Sys_error _ -> ())