matita.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \
matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \
- matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo
+ matitaEngine.cmi matitaDisambiguator.cmi buildTimeConf.cmo
matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \
- matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx
+ matitaEngine.cmx matitaDisambiguator.cmx buildTimeConf.cmx
matitaDb.cmo: matitaMisc.cmi matitaDb.cmi
matitaDb.cmx: matitaMisc.cmx matitaDb.cmi
matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi
matitac.cmo: matitacLib.cmi
matitac.cmx: matitacLib.cmx
matitacLib.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi \
- matitaEngine.cmi matitaDb.cmi buildTimeConf.cmo matitacLib.cmi
+ matitaEngine.cmi buildTimeConf.cmo matitacLib.cmi
matitacLib.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx \
- matitaEngine.cmx matitaDb.cmx buildTimeConf.cmx matitacLib.cmi
-matitaclean.cmo: matitaSync.cmi matitaMisc.cmi matitaDb.cmi
-matitaclean.cmx: matitaSync.cmx matitaMisc.cmx matitaDb.cmx
-matitadep.cmo: matitaMisc.cmi
-matitadep.cmx: matitaMisc.cmx
+ matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi
+matitaclean.cmo: matitacleanLib.cmi matitaDb.cmi
+matitaclean.cmx: matitacleanLib.cmx matitaDb.cmx
+matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaDb.cmi \
+ matitacleanLib.cmi
+matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaDb.cmx \
+ matitacleanLib.cmi
+matitadep.cmo: matitaMisc.cmi matitaExcPp.cmi
+matitadep.cmx: matitaMisc.cmx matitaExcPp.cmx
matitaDisambiguator.cmi: matitaTypes.cmo
matitaEngine.cmi: matitaTypes.cmo
matitaGtkMisc.cmi: matitaGeneratedGui.cmi
matitaMisc.cmo \
matitaDb.cmo \
matitaSync.cmo \
+ matitacleanLib.cmo \
matitaDisambiguator.cmo \
matitaEngine.cmo \
matitaScript.cmo \
matitaGeneratedGui.cmo \
matitaGtkMisc.cmo \
matitaGui.cmo \
- matitaMathView.cmo
+ matitaMathView.cmo
# objects for matitac (batch compiler)
CCMOS = \
buildTimeConf.cmo \
matitaDisambiguator.cmo \
matitaEngine.cmo \
matitacLib.cmo
+CLEANCMOS = $(CCMOS) matitacleanLib.cmo
all: matita matitac matitatop cicbrowser matitadep matitaclean
ifeq ($(HAVE_OCAMLOPT),yes)
CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
+CLEANCMXS = $(patsubst %.cmo,%.cmx,$(CLEANCMOS))
LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES))
LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES))
CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(CREQUIRES))
matitadep.opt: matitadep.ml $(DEPLIB_DEPS) $(CCMXS)
$(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(CCMXS) $<
-matitaclean: matitaclean.ml $(CLEANLIB_DEPS) $(CCMOS)
- $(OCAMLC) $(CLEANPKGS) -linkpkg -o $@ $(CCMOS) $<
-matitaclean.opt: matitaclean.ml $(CLEANLIB_DEPS) $(CCMXS)
- $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CCMXS) $<
+matitaclean: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMOS)
+ $(OCAMLC) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMOS) $<
+matitaclean.opt: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS)
+ $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $<
cicbrowser: matita
@test -f $@ || ln -s $< $@
let l = ref [] in
Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
List.map UriManager.uri_of_string !l
+
+let reset_owner_environment () =
+ clean_owner_environment ();
+ create_owner_environment ()
+
val instance: unit -> Mysql.dbd
-val clean_owner_environment : unit -> unit
-val create_owner_environment : unit -> unit
+val reset_owner_environment : unit -> unit
val remove_uri: UriManager.uri -> string list
val xpointers_of_ind: UriManager.uri -> UriManager.uri list
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 cache_of_processed_baseuri = Hashtbl.create 1024
-
-let one_step_depend suri =
- let buri =
- try
- UM.buri_of_uri (UM.uri_of_string suri)
- with UM.IllFormedUri _ -> suri
- in
- if Hashtbl.mem cache_of_processed_baseuri buri then
- []
- else
- begin
- Hashtbl.add cache_of_processed_baseuri buri true;
- let query =
- let buri = buri ^ "/" in
- let buri = Mysql.escape buri in
- let obj_tbl = MetadataTypes.obj_tbl () in
- Printf.sprintf
- "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
- in
- try
- let rc = Mysql.exec dbd query 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 *)
- end
-
-
-let safe_buri_of_suri suri =
- try
- UM.buri_of_uri (UM.uri_of_string suri)
- with
- UM.IllFormedUri _ -> suri
-
-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 safe_buri_of_suri 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
- (* 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 -> 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 u @ acc) [] uri_to_remove
- in
- let depend =
- MatitaMisc.list_uniq
- (List.fast_sort Pervasives.compare depend)
- in
- uri_to_remove, depend
-
-let buri_of_file file =
- let ic = open_in file in
- let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in
- close_in ic;
- let uri = ref "" in
- List.iter
- (function
- | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
- uri := MatitaMisc.strip_trailing_slash buri
- | _ -> ())
- stms;
- !uri
-
-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 main uri_to_remove = MatitacleanLib.clean_baseuris uri_to_remove
let usage () =
prerr_endline "";
prerr_endline "usage:";
prerr_endline "\tmatitaclean all";
- prerr_endline "\tmatitaclean dry (uri|file)+";
prerr_endline "\tmatitaclean (uri|file)+";
prerr_endline "";
exit 1
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
+ if Sys.argv.(1) = "all" then
+ begin
+ MatitaDb.reset_owner_environment ();
+ exit 0
+ end
let uri_to_remove =ref [] in
(try
- for i = start to Array.length Sys.argv - 1 do
+ for i = 1 to Array.length Sys.argv - 1 do
let suri = Sys.argv.(i) in
let uri =
try
UM.buri_of_uri (UM.uri_of_string suri)
with
- UM.IllFormedUri _ -> buri_of_file suri
+ UM.IllFormedUri _ -> MatitacleanLib.baseuri_of_file 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 prerr_endline l;
- exit 0
- end
- else
- List.iter
- (fun u ->
- prerr_endline ("Removing " ^ u);
- try
- MatitaSync.remove (UM.uri_of_string u)
- with Sys_error _ -> ())
- l
+ main !uri_to_remove
--- /dev/null
+module HGT = Http_getter_types;;
+module HG = Http_getter;;
+module UM = UriManager;;
+module TA = TacticAst;;
+
+let cache_of_processed_baseuri = Hashtbl.create 1024
+
+let one_step_depend suri =
+ let buri =
+ try
+ UM.buri_of_uri (UM.uri_of_string suri)
+ with UM.IllFormedUri _ -> suri
+ in
+ if Hashtbl.mem cache_of_processed_baseuri buri then
+ []
+ else
+ begin
+ Hashtbl.add cache_of_processed_baseuri buri true;
+ let query =
+ let buri = buri ^ "/" in
+ let buri = Mysql.escape buri in
+ let obj_tbl = MetadataTypes.obj_tbl () in
+ Printf.sprintf
+ "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
+ in
+ try
+ let rc = Mysql.exec (MatitaDb.instance ()) query 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 *)
+ end
+
+
+let safe_buri_of_suri suri =
+ try
+ UM.buri_of_uri (UM.uri_of_string suri)
+ with
+ UM.IllFormedUri _ -> suri
+
+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 safe_buri_of_suri 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
+ (* 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 -> 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 u @ acc) [] uri_to_remove
+ in
+ let depend =
+ MatitaMisc.list_uniq
+ (List.fast_sort Pervasives.compare depend)
+ in
+ uri_to_remove, depend
+
+let baseuri_of_file file =
+ let ic = open_in file in
+ let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in
+ close_in ic;
+ let uri = ref "" in
+ List.iter
+ (function
+ | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
+ uri := MatitaMisc.strip_trailing_slash buri
+ | _ -> ())
+ stms;
+ !uri
+
+let rec fix uris next =
+ match next with
+ | [] -> uris
+ | l -> let uris, next = close_uri_list l in fix uris next @ uris
+
+let clean_baseuris buris =
+ let l = fix [] buris in
+ let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in
+ let l = List.map UriManager.uri_of_string l in
+ List.iter MatitaSync.remove l
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val clean_baseuris : string list -> unit
+val baseuri_of_file : string -> string
projects / helm.git / commitdiff