From: Stefano Zacchiroli Date: Thu, 23 Feb 2006 21:35:38 +0000 (+0000) Subject: added "gragrep", grep-like tool over a bunch of grafite scripts X-Git-Tag: 0.4.95@7852~1624 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e0cf3f03dcddf705a47ded66633f3a6952759703;p=helm.git added "gragrep", grep-like tool over a bunch of grafite scripts --- diff --git a/matita/.depend b/matita/.depend index 21715bac3..300db49f5 100644 --- a/matita/.depend +++ b/matita/.depend @@ -4,14 +4,18 @@ buildTimeConf.cmo: buildTimeConf.cmi buildTimeConf.cmx: buildTimeConf.cmi dump_moo.cmo: buildTimeConf.cmi dump_moo.cmx: buildTimeConf.cmx +gragrep.cmo: matitaInit.cmi buildTimeConf.cmi gragrep.cmi +gragrep.cmx: matitaInit.cmx buildTimeConf.cmx gragrep.cmi matitaclean.cmo: matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaInit.cmx matitaclean.cmi matitacLib.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmi matitacLib.cmi matitacLib.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ buildTimeConf.cmx matitacLib.cmi -matitac.cmo: matitamake.cmi matitadep.cmi matitaclean.cmi matitacLib.cmi -matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx +matitac.cmo: matitamake.cmi matitadep.cmi matitaclean.cmi matitacLib.cmi \ + gragrep.cmi +matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx \ + gragrep.cmx matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi diff --git a/matita/Makefile b/matita/Makefile index 39b348eea..272711ad7 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -53,13 +53,17 @@ MAINCMOS = \ matitadep.cmo \ matitaclean.cmo \ matitamake.cmo \ + gragrep.cmo \ $(NULL) -PROGRAMS_BYTE = matita matitac cicbrowser matitadep matitaclean matitamake dump_moo +PROGRAMS_BYTE = \ + matita matitac cicbrowser matitadep matitaclean matitamake PROGRAMS = $(PROGRAMS_BYTE) matitatop PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) +NOINST_PROGRAMS = dump_moo gragrep +NOINST_PROGRAMS_OPT = $(patsubst %,%.opt,$(EXTRA_PROGRAMS)) .PHONY: all -all: $(PROGRAMS) +all: $(PROGRAMS) $(NOINST_PROGRAMS) # all: matita.conf.xml $(PROGRAMS) coq.moo # matita.conf.xml: matita.conf.xml.sample @@ -87,7 +91,7 @@ LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES)) CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_CREQUIRES)) CLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_CREQUIRES)) -opt: $(PROGRAMS_OPT) +opt: $(PROGRAMS_OPT) $(NOINST_PROGRAMS_OPT) upx: $(PROGRAMS_UPX) .PHONY: opt upx @@ -137,6 +141,11 @@ matitamake: matitac matitamake.opt: matitac.opt @test -f $@ || ln -s $< $@ +gragrep: matitac + @test -f $@ || ln -s $< $@ +gragrep.opt: matitac.opt + @test -f $@ || ln -s $< $@ + cicbrowser: matita @test -f $@ || ln -s $< $@ cicbrowser.opt: matita.opt @@ -149,8 +158,8 @@ matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade .PHONY: clean clean: rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ - $(PROGRAMS) \ - $(PROGRAMS_OPT) \ + $(PROGRAMS) $(PROGRAMS_OPT) \ + $(NOINST_PROGRAMS) $(NOINST_PROGRAMS_OPT) \ $(PROGRAMS_STATIC) \ $(PROGRAMS_UPX) \ $(NULL) diff --git a/matita/gragrep.ml b/matita/gragrep.ml new file mode 100644 index 000000000..d44c08d27 --- /dev/null +++ b/matita/gragrep.ml @@ -0,0 +1,67 @@ +(* Copyright (C) 2006, 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/ + *) + +open Printf + +let is_notation = function GrafiteParser.LNone _ -> true | _ -> false + +let grep () = + let recursive = ref false in + let spec = [ + "-r", Arg.Set recursive, "enable directory recursion"; + ] in + MatitaInit.add_cmdline_spec spec; + MatitaInit.initialize_all (); + let include_paths = + Helm_registry.get_list Helm_registry.string "matita.includes" in + let status = + CicNotation2.load_notation ~include_paths + BuildTimeConf.core_notation_script in + let path = + match Helm_registry.get_list Helm_registry.string "matita.args" with + | [ path ] -> path + | _ -> MatitaInit.die_usage () in + let grep_fun = + if !recursive then + (fun dirname -> + ignore (GrafiteWalker.rgrep_statement ~status + ~callback:(fun (fname, s) -> printf "%s: %s\n%!" fname s) + ~dirname is_notation)) + else + (fun fname -> + ignore (GrafiteWalker.grep_statement ~status + ~callback:(fun s -> printf "%s\n%!" s) + ~fname is_notation)) in + grep_fun path + +let handle_localized_exns f arg = + try + f arg + with HExtlib.Localized (loc, exn) -> + let loc_begin, loc_end = HExtlib.loc_of_floc loc in + eprintf "Error at %d-%d: %s\n%!" loc_begin loc_end (Printexc.to_string exn) + +let main () = handle_localized_exns grep () + diff --git a/matita/gragrep.mli b/matita/gragrep.mli new file mode 100644 index 000000000..f762adb22 --- /dev/null +++ b/matita/gragrep.mli @@ -0,0 +1,27 @@ +(* Copyright (C) 2006, 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 main: unit -> unit + diff --git a/matita/matitac.ml b/matita/matitac.ml index 95b500b87..05add3ce4 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -27,6 +27,7 @@ let main () = match Filename.basename Sys.argv.(0) with + | "gragrep" | "gragrep.opt" -> Gragrep.main () | "matitadep" | "matitadep.opt" -> Matitadep.main () | "matitaclean" | "matitaclean.opt" -> Matitaclean.main () | "matitamake" | "matitamake.opt" -> Matitamake.main ()