From: Stefano Zacchiroli Date: Thu, 3 Nov 2005 15:00:47 +0000 (+0000) Subject: better dependencies among modules and symlinking of several matitatools to a single... X-Git-Tag: V_0_7_2_3~147 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6fa89cef6aa8fc1774db065a9fcfc47867579054;p=helm.git better dependencies among modules and symlinking of several matitatools to a single one in order to reduce global size of matita executables --- diff --git a/helm/matita/.cvsignore b/helm/matita/.cvsignore index babd18569..db41158de 100644 --- a/helm/matita/.cvsignore +++ b/helm/matita/.cvsignore @@ -1,4 +1,3 @@ -matita.conf.xml *.a *.annot autom4te.cache @@ -14,29 +13,32 @@ config.log config.status configure .depend +dump_moo +gtkmathview.matita.conf.xml Makefile matita .matita matitac +matitaclean +matitaclean.opt +matita.conf.xml +matita.conf.xml +matita.conf.xml.sample matitac.opt +matitadep +matitadep.opt matitaGeneratedGui.ml matitaGeneratedGui.mli matita.glade.bak matita.gladep matita.gladep.bak +matitamake +matitamake.opt matita.opt matita.opt matitatop -matitadep -matitadep.opt -matitaclean -matitaclean.opt -matitamake -matitamake.opt -dump_moo +*.moo *.o +*.static *.swp -matita.conf.xml -*.moo -matita.conf.xml.sample -gtkmathview.matita.conf.xml +*.upx diff --git a/helm/matita/.depend b/helm/matita/.depend index d4bad9404..f6d37dcf8 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,25 +1,27 @@ dump_moo.cmo: matitaMoo.cmi matitaLog.cmi buildTimeConf.cmo dump_moo.cmx: matitaMoo.cmx matitaLog.cmx buildTimeConf.cmx matitacleanLib.cmo: matitaSync.cmi matitaMoo.cmi matitaMisc.cmi matitaLog.cmi \ - matitaDb.cmi matitacleanLib.cmi + matitaExcPp.cmi matitaDb.cmi buildTimeConf.cmo matitacleanLib.cmi matitacleanLib.cmx: matitaSync.cmx matitaMoo.cmx matitaMisc.cmx matitaLog.cmx \ - matitaDb.cmx matitacleanLib.cmi + matitaExcPp.cmx matitaDb.cmx buildTimeConf.cmx matitacleanLib.cmi matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi \ - matitaInit.cmi matitaDb.cmi + matitaInit.cmi matitaDb.cmi matitaclean.cmi matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx \ - matitaInit.cmx matitaDb.cmx + matitaInit.cmx matitaDb.cmx matitaclean.cmi matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMoo.cmi \ - matitaMisc.cmi matitaLog.cmi matitaInit.cmi matitaExcPp.cmi \ - matitaEngine.cmi matitaDb.cmi buildTimeConf.cmo matitacLib.cmi + matitaLog.cmi matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ + matitaDb.cmi buildTimeConf.cmo matitacLib.cmi matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMoo.cmx \ - matitaMisc.cmx matitaLog.cmx matitaInit.cmx matitaExcPp.cmx \ - matitaEngine.cmx matitaDb.cmx buildTimeConf.cmx matitacLib.cmi -matitac.cmo: matitacLib.cmi -matitac.cmx: matitacLib.cmx + matitaLog.cmx matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ + matitaDb.cmx buildTimeConf.cmx matitacLib.cmi +matitac.cmo: matitamake.cmo matitadep.cmi matitaclean.cmi matitacLib.cmi +matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx matitaDb.cmo: matitaMisc.cmi matitaDb.cmi matitaDb.cmx: matitaMisc.cmx matitaDb.cmi -matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaInit.cmi -matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaInit.cmx +matitadep.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaInit.cmi \ + matitadep.cmi +matitadep.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaInit.cmx \ + matitadep.cmi matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi matitaEngine.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.cmi \ @@ -50,24 +52,22 @@ matitaLog.cmo: matitaLog.cmi matitaLog.cmx: matitaLog.cmi matitamakeLib.cmo: matitaLog.cmi buildTimeConf.cmo matitamakeLib.cmi matitamakeLib.cmx: matitaLog.cmx buildTimeConf.cmx matitamakeLib.cmi -matitamake.cmo: matitamakeLib.cmi matitaInit.cmi -matitamake.cmx: matitamakeLib.cmx matitaInit.cmx +matitamake.cmo: matitamakeLib.cmi buildTimeConf.cmo +matitamake.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaLog.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \ buildTimeConf.cmo matitaMathView.cmi matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaLog.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \ buildTimeConf.cmx matitaMathView.cmi -matitaMisc.cmo: matitaTypes.cmi matitaLog.cmi matitaExcPp.cmi \ - buildTimeConf.cmo matitaMisc.cmi -matitaMisc.cmx: matitaTypes.cmx matitaLog.cmx matitaExcPp.cmx \ - buildTimeConf.cmx matitaMisc.cmi -matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ - matitaMathView.cmi matitaLog.cmi matitaInit.cmi matitaGui.cmi \ - matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo -matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaMathView.cmx matitaLog.cmx matitaInit.cmx matitaGui.cmx \ - matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx +matitaMisc.cmo: matitaTypes.cmi buildTimeConf.cmo matitaMisc.cmi +matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi +matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi matitaLog.cmi \ + matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi matitaEngine.cmi \ + buildTimeConf.cmo +matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx matitaLog.cmx \ + matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx matitaEngine.cmx \ + buildTimeConf.cmx matitaMoo.cmo: matitaTypes.cmi matitaMoo.cmi matitaMoo.cmx: matitaTypes.cmx matitaMoo.cmi matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \ @@ -88,7 +88,6 @@ matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaGui.cmi: matitaGuiTypes.cmi matitaDisambiguator.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaLog.cmi matitaGeneratedGui.cmi matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi -matitaMisc.cmi: matitaTypes.cmi matitaMoo.cmi: matitaTypes.cmi matitaScript.cmi: matitaTypes.cmi matitaSync.cmi: matitaTypes.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index c1e1c094e..b1239778c 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -11,6 +11,7 @@ REQUIRES = @FINDLIB_REQUIRES@ CREQUIRES = @FINDLIB_CREQUIRES@ DEPREQUIRES = @FINDLIB_DEPREQUIRES@ CLEANREQUIRES = @FINDLIB_CLEANREQUIRES@ +MAKEREQUIRES = @FINDLIB_MAKEREQUIRES@ HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ OCAML_FLAGS = -pp $(CAMLP4O) @@ -18,6 +19,7 @@ PKGS = -package "$(REQUIRES)" CPKGS = -package "$(CREQUIRES)" DEPPKGS = -package "$(DEPREQUIRES)" CLEANPKGS = -package "$(CLEANREQUIRES)" +MAKEPKGS = -package "$(MAKEREQUIRES)" OCAML_THREADS_FLAGS = -thread OCAML_DEBUG_FLAGS = -g OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) @@ -26,6 +28,7 @@ OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) STATIC_LINK = dist/static_link/static_link +# for matita STATIC_LIBS = \ t1 t1x \ gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \ @@ -35,7 +38,13 @@ STATIC_LIBS = \ mysqlclient \ expat \ $(NULL) -STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++ -cclib -lart_lgpl_2 +STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++ +# for matitac & co +STATIC_CLIBS = \ + gdome \ + mysqlclient \ + $(NULL) +STATIC_EXTRA_CLIBS = MATITA_FLAGS = NODB=false @@ -82,12 +91,23 @@ CCMOS = \ matitaEngine.cmo \ matitacLib.cmo \ $(NULL) +MAINCMOS = \ + matitadep.cmo \ + matitaclean.cmo \ + matitamake.cmo \ + $(NULL) +DEPCMOS = $(CCMOS) CLEANCMOS = $(CCMOS) -MAKECMOS = $(CCMOS) +MAKECMOS = \ + buildTimeConf.cmo \ + matitaLog.cmo \ + matitamakeLib.cmo \ + $(NULL) PROGRAMS_BYTE = matita matitac cicbrowser matitadep matitaclean matitamake dump_moo PROGRAMS = $(PROGRAMS_BYTE) matitatop PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT)) +PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC)) all: matita.conf.xml $(PROGRAMS) coq.moo @@ -119,6 +139,8 @@ coq.moo.opt: coq.ma matitac.opt ifeq ($(HAVE_OCAMLOPT),yes) CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) +MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS)) +DEPCMXS = $(patsubst %.cmo,%.cmx,$(DEPCMOS)) CLEANCMXS = $(patsubst %.cmo,%.cmx,$(CLEANCMOS)) MAKECMXS = $(patsubst %.cmo,%.cmx,$(MAKECMOS)) LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES)) @@ -133,8 +155,10 @@ MAKELIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format MAKELIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MAKEREQUIRES)) opt: $(PROGRAMS_OPT) coq.moo.opt static: $(PROGRAMS_STATIC) coq.moo.opt - strip *.static +upx: $(PROGRAMS_UPX) coq.moo.opt else +upx: + @echo "Native code compilation is disabled" opt: @echo "Native code compilation is disabled" static: @@ -149,54 +173,78 @@ matita.opt.static: $(LIBX_DEPS) $(CMXS) matita.ml $(STATIC_LINK) $(STATIC_LIBS) -- \ $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \ $(STATIC_EXTRA_LIBS) + strip $@ dump_moo: buildTimeConf.cmo matitaLog.cmo matitaMoo.cmo dump_moo.ml $(OCAMLC) $(PKGS) -linkpkg -o $@ $^ dump_moo.opt: buildTimeConf.cmx matitaLog.cmx matitaMoo.cmx dump_moo.ml $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ dump_moo.opt.static: buildTimeConf.cmx matitaLog.cmx matitaMoo.cmx dump_moo.ml - $(STATIC_LINK) $(STATIC_LIBS) -- \ + $(STATIC_LINK) $(STATIC_CLIBS) -- \ $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \ - $(STATIC_EXTRA_LIBS) + $(STATIC_EXTRA_CLIBS) + strip $@ -matitac: $(CLIB_DEPS) $(CCMOS) matitac.ml - $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) matitac.ml -matitac.opt: $(CLIBX_DEPS) $(CCMXS) matitac.ml - $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml -matitac.opt.static: $(CLIBX_DEPS) $(CCMXS) matitac.ml - $(STATIC_LINK) $(STATIC_LIBS) -- \ - $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml \ - $(STATIC_EXTRA_LIBS) +matitac: $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) matitac.ml + $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml +matitac.opt: $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml + $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml +matitac.opt.static: $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml + $(STATIC_LINK) $(STATIC_CLIBS) -- \ + $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \ + $(STATIC_EXTRA_CLIBS) + strip $@ matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS) $(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $< -matitadep: matitadep.ml $(DEPLIB_DEPS) $(CCMOS) - $(OCAMLC) $(DEPPKGS) -linkpkg -o $@ $(CCMOS) $< -matitadep.opt: matitadep.ml $(DEPLIB_DEPS) $(CCMXS) - $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(CCMXS) $< -matitadep.opt.static: matitadep.ml $(DEPLIB_DEPS) $(CCMXS) - $(STATIC_LINK) $(STATIC_LIBS) -- \ - $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(CCMXS) $< \ - $(STATIC_EXTRA_LIBS) +# matitadep: matitadep.ml $(DEPLIB_DEPS) $(DEPCMOS) +# $(OCAMLC) $(DEPPKGS) -linkpkg -o $@ $(DEPCMOS) $< +# matitadep.opt: matitadep.ml $(DEPLIB_DEPS) $(DEPCMXS) +# $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(DEPCMXS) $< +# matitadep.opt.static: matitadep.ml $(DEPLIB_DEPS) $(DEPCMXS) +# $(STATIC_LINK) $(STATIC_CLIBS) -- \ +# $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(DEPCMXS) $< \ +# $(STATIC_EXTRA_CLIBS) +# strip $@ +matitadep: matitac + @test -f $@ || ln -s $< $@ +matitadep.opt: matitac.opt + @test -f $@ || ln -s $< $@ +matitadep.opt.static: matitac.opt.static + @test -f $@ || ln -s $< $@ -matitaclean: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMOS) - $(OCAMLC) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMOS) $< -matitaclean.opt: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS) - $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $< -matitaclean.opt.static: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS) - $(STATIC_LINK) $(STATIC_LIBS) -- \ - $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $< \ - $(STATIC_EXTRA_LIBS) +# matitaclean: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMOS) +# $(OCAMLC) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMOS) $< +# matitaclean.opt: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS) +# $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $< +# matitaclean.opt.static: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS) +# $(STATIC_LINK) $(STATIC_CLIBS) -- \ +# $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $< \ +# $(STATIC_EXTRA_CLIBS) +# strip $@ +matitaclean: matitac + @test -f $@ || ln -s $< $@ +matitaclean.opt: matitac.opt + @test -f $@ || ln -s $< $@ +matitaclean.opt.static: matitac.opt.static + @test -f $@ || ln -s $< $@ -matitamake: matitamake.ml $(MAKECMOS) - $(OCAMLC) $(PKGS) -linkpkg -o $@ $(MAKECMOS) $< -matitamake.opt: matitamake.ml $(MAKECMXS) - $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(MAKECMXS) $< -matitamake.opt.static: matitamake.ml $(MAKECMXS) - $(STATIC_LINK) $(STATIC_LIBS) -- \ - $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(MAKECMXS) $< \ - $(STATIC_EXTRA_LIBS) +# matitamake: matitamake.ml $(MAKECMOS) +# $(OCAMLC) $(MAKEPKGS) -linkpkg -o $@ $(MAKECMOS) $< +# matitamake.opt: matitamake.ml $(MAKECMXS) +# $(OCAMLOPT) $(MAKEPKGS) -linkpkg -o $@ $(MAKECMXS) $< +# matitamake.opt.static: matitamake.ml $(MAKECMXS) +# $(STATIC_LINK) $(STATIC_CLIBS) -- \ +# $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(MAKECMXS) $< \ +# $(STATIC_EXTRA_CLIBS) +# strip $@ +matitamake: matitac + @test -f $@ || ln -s $< $@ +matitamake.opt: matitac.opt + @test -f $@ || ln -s $< $@ +matitamake.opt.static: matitac.opt.static + @test -f $@ || ln -s $< $@ cicbrowser: matita @test -f $@ || ln -s $< $@ @@ -204,6 +252,8 @@ cicbrowser.opt: matita.opt @test -f $@ || ln -s $< $@ cicbrowser.opt.static: matita.opt.static @test -f $@ || ln -s $< $@ +cicbrowser.opt.static.upx: matita.opt.static.upx + @test -f $@ || ln -s $< $@ matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade $(LABLGLADECC) -embed $< > matitaGeneratedGui.ml @@ -218,11 +268,17 @@ matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade %.annot: %.ml $(OCAMLC) -dtypes $(PKGS) -c $< +%.upx: % + cp $< $@ + strip $@ + upx $@ + clean: rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ $(PROGRAMS) \ $(PROGRAMS_OPT) \ $(PROGRAMS_STATIC) \ + $(PROGRAMS_UPX) \ $(NULL) distclean: clean rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index 012b54793..4f8c991d1 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -26,22 +26,25 @@ if test $HAVE_CAMLP4O = "yes"; then else AC_MSG_ERROR(could not find camlp4o) fi -FINDLIB_DEPREQUIRES="\ +FINDLIB_COMREQUIRES="\ pcre \ mysql \ helm-registry \ helm-extlib \ helm-hmysql \ +helm-cic_notation \ +helm-tactics \ helm-cic_disambiguation \ -helm-paramodulation \ " -FINDLIB_CLEANREQUIRES="$FINDLIB_DEPREQUIRES" -FINDLIB_CREQUIRES="\ -$FINDLIB_CLEANREQUIRES \ -unix \ -helm-cic_omdoc \ -helm-tactics \ -helm-xml \ +FINDLIB_CLEANREQUIRES="$FINDLIB_COMREQUIRES" +FINDLIB_DEPREQUIRES="$FINDLIB_COMREQUIRES" +FINDLIB_MAKEREQUIRES=" \ +helm-registry \ +helm-extlib \ +" +FINDLIB_CREQUIRES=" \ +$FINDLIB_COMREQUIRES \ +helm-paramodulation \ " FINDLIB_REQUIRES="\ $FINDLIB_CREQUIRES \ @@ -49,7 +52,10 @@ lablgtk2.glade \ lablgtkmathview \ lablgtksourceview \ helm-xmldiff \ +helm-cic_transformations \ helm-tactics \ +helm-cic_disambiguation \ +helm-paramodulation \ " for r in $FINDLIB_REQUIRES do @@ -104,6 +110,7 @@ AC_SUBST(FINDLIB_REQUIRES) AC_SUBST(FINDLIB_CREQUIRES) AC_SUBST(FINDLIB_DEPREQUIRES) AC_SUBST(FINDLIB_CLEANREQUIRES) +AC_SUBST(FINDLIB_MAKEREQUIRES) AC_SUBST(HAVE_OCAMLOPT) AC_SUBST(LABLGLADECC) AC_SUBST(OCAMLFIND) diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index ecb2e4061..3c664c43c 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -677,10 +677,10 @@ - + 350 250 - Interpretation choice + title GTK_WINDOW_TOPLEVEL GTK_WIN_POS_NONE True @@ -706,7 +706,7 @@ GTK_BUTTONBOX_END - + True True True @@ -719,7 +719,7 @@ - + True True True @@ -732,7 +732,7 @@ - + True True True @@ -759,7 +759,7 @@ 0 - + True some informative message here ... False @@ -793,7 +793,7 @@ GTK_CORNER_TOP_LEFT - + True True False diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index b9e09f24d..dd8d6d83d 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -30,7 +30,8 @@ open MatitaTypes (** {2 Initialization} *) -let _ = MatitaInit.initialize_all () +let _ = MatitaInit.initialize_all () +let _ = Paramodulation.Saturation.init () (* ALB to link paramodulation *) (** {2 GUI callbacks} *) @@ -153,7 +154,16 @@ let _ = (List.map (fun (g, _, _) -> string_of_int g) (MatitaScript.current ())#proofMetasenv)); prerr_endline ("stack: " ^ Continuationals.Stack.pp - (MatitaMisc.get_stack (MatitaScript.current ())#status))); + (MatitaTypes.get_stack (MatitaScript.current ())#status))); +(* addDebugItem "ask record choice" + (fun _ -> + MatitaLog.debug (string_of_int + (MatitaGtkMisc.ask_record_choice ~gui ~title:"title" ~message:"msg" + ~fields:["a"; "b"; "c"] + ~records:[ + ["0"; "0"; "0"]; ["0"; "0"; "1"]; ["0"; "1"; "0"]; ["0"; "1"; "1"]; + ["1"; "0"; "0"]; ["1"; "0"; "1"]; ["1"; "1"; "0"]; ["1"; "1"; "1"]] + ()))); *) addDebugItem "rotate light bulbs" (fun _ -> let nb = gui#main#hintNotebook in diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 9595df931..1d3b1f94e 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -161,13 +161,13 @@ let disambiguate_term ?context status_ref goal term = let context = match context with | Some c -> c - | None -> MatitaMisc.get_proof_context status goal + | None -> MatitaTypes.get_proof_context status goal in let (diff, metasenv, cic, _) = singleton (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) ~aliases:status.aliases ~universe:(Some status.multi_aliases) - ~context ~metasenv:(MatitaMisc.get_proof_metasenv status) term) + ~context ~metasenv:(MatitaTypes.get_proof_metasenv status) term) in let status = MatitaTypes.set_metasenv metasenv status in let status = MatitaSync.set_proof_aliases status diff in @@ -455,13 +455,13 @@ let classify_tactic tactic = let apply_tactic tactic (status, goal) = (* prerr_endline "apply_tactic"; *) -(* prerr_endline (Continuationals.Stack.pp (MatitaMisc.get_stack status)); *) - let starting_metasenv = MatitaMisc.get_proof_metasenv status in +(* prerr_endline (Continuationals.Stack.pp (MatitaTypes.get_stack status)); *) + let starting_metasenv = MatitaTypes.get_proof_metasenv status in let before = List.map (fun g, _, _ -> g) starting_metasenv in (* prerr_endline "disambiguate"; *) let status_ref, tactic = disambiguate_tactic status goal tactic in - let metasenv_after_refinement = MatitaMisc.get_proof_metasenv !status_ref in - let proof = MatitaMisc.get_current_proof !status_ref in + let metasenv_after_refinement = MatitaTypes.get_proof_metasenv !status_ref in + let proof = MatitaTypes.get_current_proof !status_ref in let proof_status = proof, goal in let needs_reordering, always_opens_a_goal = classify_tactic tactic in let tactic = tactic_of_ast tactic in @@ -515,10 +515,10 @@ struct let apply_tactic tac = tac let goals (_, opened, closed) = opened, closed let set_goals (opened, closed) (status, _, _) = (status, opened, closed) - let get_stack (status, _) = MatitaMisc.get_stack status + let get_stack (status, _) = MatitaTypes.get_stack status let set_stack stack (status, opened, closed) = - MatitaMisc.set_stack stack status, opened, closed + MatitaTypes.set_stack stack status, opened, closed let inject (status, _) = (status, [], []) let focus goal (status, _, _) = (status, goal) @@ -675,7 +675,7 @@ let disambiguate_obj status obj = match obj with GrafiteAst.Inductive (_,(name,_,_,_)::_) | GrafiteAst.Record (_,name,_,_) -> - Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind")) + Some (UriManager.uri_of_string (MatitaTypes.qualify status name ^ ".ind")) | GrafiteAst.Inductive _ -> assert false | GrafiteAst.Theorem _ -> None in let (diff, metasenv, cic, _) = @@ -744,7 +744,7 @@ let eval_command opts status cmd = add_moo_content [cmd] status | GrafiteAst.Include (loc, path) -> let absolute_path = make_absolute opts.include_paths path in - let moopath = MatitaMisc.obj_file_of_script absolute_path in + let moopath = MatitacleanLib.obj_file_of_script absolute_path in let status = ref status in if not (Sys.file_exists moopath) then raise (IncludedFileNotCompiled moopath); @@ -836,9 +836,9 @@ let eval_command opts status cmd = (match types with (name,_,_,_)::_ -> name | _ -> assert false) | _ -> assert false in let uri = - UriManager.uri_of_string (MatitaMisc.qualify status name ^ ext) + UriManager.uri_of_string (MatitaTypes.qualify status name ^ ext) in - let metasenv = MatitaMisc.get_proof_metasenv status in + let metasenv = MatitaTypes.get_proof_metasenv status in match obj with | Cic.CurrentProof (_,metasenv',bo,ty,_,_) -> let name = UriManager.name_of_uri uri in diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index 0ad36dfee..3c0d1b4c3 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -165,7 +165,6 @@ class stringListModel (tree_view: GTree.view) = List.map (function [x] -> x | _ -> assert false) m end - class taggedStringListModel ~(tags:(string * GdkPixbuf.pixbuf) list) (tree_view: GTree.view) = @@ -206,10 +205,54 @@ class taggedStringListModel ~(tags:(string * GdkPixbuf.pixbuf) list) tree_view#selection#get_selected_rows end +class recordModel (tree_view:GTree.view) = + let cols_list = new GTree.column_list in + let text_col = cols_list#add Gobject.Data.string in +(* let combo_col = cols_list#add (Gobject.Data.gobject_by_name "GtkListStore") in *) + let combo_col = cols_list#add Gobject.Data.int in + let toggle_col = cols_list#add Gobject.Data.boolean in + let list_store = GTree.list_store cols_list in + let text_rend = (GTree.cell_renderer_text [], ["text", text_col]) in + let combo_rend = GTree.cell_renderer_combo [] in +(* let combo_rend = (GTree.cell_renderer_combo [], [|+"model", combo_col+|]) in *) + let toggle_rend = + (GTree.cell_renderer_toggle [`ACTIVATABLE true], ["active", toggle_col]) + in + let text_vcol = GTree.view_column ~renderer:text_rend () in + let combo_vcol = GTree.view_column ~renderer:(combo_rend, []) () in + let _ = + combo_vcol#set_cell_data_func combo_rend + (fun _ _ -> + prerr_endline "qui"; + let model, col = + GTree.store_of_list Gobject.Data.string ["a"; "b"; "c"] + in + combo_rend#set_properties [ + `MODEL (Some (model :> GTree.model)); + `TEXT_COLUMN col + ]) + in + let toggle_vcol = GTree.view_column ~renderer:toggle_rend () in + object (self) + initializer + tree_view#set_model (Some (list_store :> GTree.model)); + ignore (tree_view#append_column text_vcol); + ignore (tree_view#append_column combo_vcol); + ignore (tree_view#append_column toggle_vcol) + + method list_store = list_store + + method easy_append s (combo:int) (toggle:bool) = + let tree_iter = list_store#append () in + list_store#set ~row:tree_iter ~column:text_col s; + list_store#set ~row:tree_iter ~column:combo_col combo; + list_store#set ~row:tree_iter ~column:toggle_col toggle + end + class type gui = object method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog - method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog + method newRecordDialog: unit -> MatitaGeneratedGui.recordChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog end @@ -307,12 +350,12 @@ let report_error ~title ~message ?parent () = | PopupClosed -> () -let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) +let ask_text ~(gui:#gui) ?(title = "") ?(message = "") ?(multiline = false) ?default () = let dialog = gui#newEmptyDialog () in dialog#emptyDialog#set_title title; - dialog#emptyDialogLabel#set_label msg; + dialog#emptyDialogLabel#set_label message; let result = ref None in let return r = result := r; @@ -351,3 +394,50 @@ let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) GtkThread.main (); (match !result with None -> raise Cancel | Some r -> r) +type combo_status = Free of string | Locked of string + +let ask_record_choice ~(gui:#gui) ?(title= "") ?(message = "") + ~fields ~records () += + let fields = Array.of_list fields in + let fields_no = Array.length fields in + assert (fields_no > 0); + let dialog = gui#newRecordDialog () in + dialog#recordChoiceDialog#set_title title; + dialog#recordChoiceDialogLabel#set_label message; + let model = new recordModel dialog#recordChoiceTreeView in + dialog#recordChoiceTreeView#set_headers_visible true; + let combos = + Array.init fields_no + (fun _ -> GTree.store_of_list Gobject.Data.string ["a"; "b"; "c"]) + in + let (store, col) = combos.(0) in + store#set ~row:(store#append ()) ~column:col "uno"; + store#set ~row:(store#append ()) ~column:col "due"; + let toggles = Array.init fields_no (fun _ -> false) in + Array.iteri + (fun i f -> model#easy_append f i toggles.(i)) + fields; + let status = Array.map (fun s -> Free s) fields in + let record_no = ref None in + let return _ = + dialog#recordChoiceDialog#destroy (); + GMain.Main.quit () + in + let fail _ = record_no := None; return () in + ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#recordChoiceOkButton (fun _ -> + match !record_no with None -> () | Some _ -> return ()); + connect_button dialog#recordChoiceCancelButton fail; +(* ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ -> + interp_no := Some (model#get_interp_no path); + return ())); + let selection = dialog#recordChoiceTreeView#selection in + ignore (selection#connect#changed (fun _ -> + match selection#get_selected_rows with + | [path] -> interp_no := Some (model#get_interp_no path) + | _ -> assert false)); *) + dialog#recordChoiceDialog#show (); + GtkThread.main (); + (match !record_no with Some n -> n | _ -> raise MatitaTypes.Cancel) + diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index e5d0e9be9..1affd2a39 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -113,31 +113,45 @@ class taggedStringListModel: class type gui = object (* minimal gui object requirements *) method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog - method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog + method newRecordDialog: unit -> MatitaGeneratedGui.recordChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog end - (** {3 Dialogs} *) + (** {3 Dialogs} + * In functions below: + * @param title window title + * @param message content of the text label shown to the user *) - (* @param parent to center the window on it *) + (** @param parent to center the window on it *) val ask_confirmation: - title:string -> - message:string -> + title:string -> message:string -> ?parent:#GWindow.window_skel -> - unit -> [`YES | `NO | `CANCEL] - -val report_error: - title:string -> - message:string -> - ?parent:#GWindow.window_skel -> - unit -> unit + unit -> + [`YES | `NO | `CANCEL] (** @param multiline (default: false) if true a TextView widget will be used * for prompting the user otherwise a TextEntry widget will be * @return the string given by the user *) val ask_text: gui:#gui -> - ?title:string -> ?msg:string -> ?multiline:bool -> ?default:string -> unit -> + ?title:string -> ?message:string -> + ?multiline:bool -> ?default:string -> unit -> string + (** @param fields field names + * @param records list of records, each record is a list of [fields] strings + * @return number of the chosen record, 0 for the first one *) +val ask_record_choice: + gui:#gui -> + ?title:string -> ?message:string -> + fields:string list -> records:string list list -> + unit -> + int + +val report_error: + title:string -> message:string -> + ?parent:#GWindow.window_skel -> + unit -> + unit + diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index bf25a5493..d4157677f 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -67,14 +67,14 @@ let clean_current_baseuri status = let ask_and_save_moo_if_needed parent fname status = let save () = - let moo_fname = MatitaMisc.obj_file_of_script fname in + let moo_fname = MatitacleanLib.obj_file_of_script fname in MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in if (MatitaScript.current ())#eos && status.MatitaTypes.proof_status = MatitaTypes.No_proof then begin let mooname = - MatitaMisc.obj_file_of_script fname + MatitacleanLib.obj_file_of_script fname in let rc = MatitaGtkMisc.ask_confirmation @@ -882,8 +882,8 @@ class gui () = dialog#check_widgets (); dialog - method newInterpDialog () = - let dialog = new interpChoiceDialog () in + method newRecordDialog () = + let dialog = new recordChoiceDialog () in dialog#check_widgets (); dialog @@ -1095,30 +1095,30 @@ class interpModel = let interactive_interp_choice () choices = let gui = instance () in assert (choices <> []); - let dialog = gui#newInterpDialog () in - let model = new interpModel dialog#interpChoiceTreeView choices in + let dialog = gui#newRecordDialog () in + let model = new interpModel dialog#recordChoiceTreeView choices in let interp_len = List.length (List.hd choices) in - dialog#interpChoiceDialog#set_title "Interpretation choice"; - dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:"; + dialog#recordChoiceDialog#set_title "Interpretation choice"; + dialog#recordChoiceDialogLabel#set_label "Choose an interpretation:"; let interp_no = ref None in let return _ = - dialog#interpChoiceDialog#destroy (); + dialog#recordChoiceDialog#destroy (); GMain.Main.quit () in let fail _ = interp_no := None; return () in - ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true)); - connect_button dialog#interpChoiceOkButton (fun _ -> + ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#recordChoiceOkButton (fun _ -> match !interp_no with None -> () | Some _ -> return ()); - connect_button dialog#interpChoiceCancelButton fail; - ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ -> + connect_button dialog#recordChoiceCancelButton fail; + ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ -> interp_no := Some (model#get_interp_no path); return ())); - let selection = dialog#interpChoiceTreeView#selection in + let selection = dialog#recordChoiceTreeView#selection in ignore (selection#connect#changed (fun _ -> match selection#get_selected_rows with | [path] -> interp_no := Some (model#get_interp_no path) | _ -> assert false)); - dialog#interpChoiceDialog#show (); + dialog#recordChoiceDialog#show (); GtkThread.main (); (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel) diff --git a/helm/matita/matitaGuiTypes.mli b/helm/matita/matitaGuiTypes.mli index cf738cd85..99b90495f 100644 --- a/helm/matita/matitaGuiTypes.mli +++ b/helm/matita/matitaGuiTypes.mli @@ -62,7 +62,7 @@ object method newBrowserWin: unit -> browserWin method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog - method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog + method newRecordDialog: unit -> MatitaGeneratedGui.recordChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml index e69c22cf8..9ea9e07d2 100644 --- a/helm/matita/matitaInit.ml +++ b/helm/matita/matitaInit.ml @@ -26,8 +26,7 @@ open Printf type thingsToInitilaize = - ConfigurationFile | Db | Environment | Getter | Notation | - Paramodulation | Makelib | CmdLine + ConfigurationFile | Db | Environment | Getter | Notation | Makelib | CmdLine exception FailedToInitialize of thingsToInitilaize @@ -61,16 +60,6 @@ let initialize_db init_status = else init_status -let initialize_paramodulation init_status = - wants [] init_status; - if not (already_configured [Paramodulation] init_status) then - begin - Paramodulation.Saturation.init (); - Paramodulation::init_status - end - else - init_status - let initialize_makelib init_status = wants [ConfigurationFile] init_status; if not (already_configured [Makelib] init_status) then @@ -207,13 +196,15 @@ let die_usage () = let initialize_all () = status := - initialize_notation + List.fold_left (fun s f -> f s) !status + [ parse_cmdline; load_configuration; initialize_makelib; + initialize_db; initialize_environment; initialize_notation ] +(* initialize_notation (initialize_environment (initialize_db - (initialize_paramodulation - (initialize_makelib - (load_configuration - (parse_cmdline !status)))))) + (initialize_makelib + (load_configuration + (parse_cmdline !status))))) *) let load_configuration_file () = status := load_configuration !status diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 1ad4b2cd1..f9c617385 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -62,9 +62,27 @@ let near (x1, y1) (x2, y2) = let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in (distance < 4.) +let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink" +let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm" let href_ds = Gdome.domString "href" let xref_ds = Gdome.domString "xref" +let domImpl = Gdome.domImplementation () + + (** Gdome.element of a MathML document whose rendering should be blank. Used + * by cicBrowser to render "about:blank" document *) +let empty_mathml = lazy ( + domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns) + ~qualifiedName:(Gdome.domString "math") ~doctype:None) + +let empty_boxml = lazy ( + domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) + ~qualifiedName:(Gdome.domString "box") ~doctype:None) + + (** shown for goals closed by side effects *) +let closed_goal_mathml = lazy ( + domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ()) + (* ids_to_terms should not be passed here, is just for debugging *) let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types = let find_parent id ids = @@ -190,11 +208,11 @@ object (self) (match self#get_element_at x y with | None -> () | Some elt -> - let namespaceURI = DomMisc.xlink_ns in let localName = href_ds in - if elt#hasAttributeNS ~namespaceURI ~localName then + if elt#hasAttributeNS ~namespaceURI:xlink_ns ~localName then self#invoke_href_callback - (elt#getAttributeNS ~namespaceURI ~localName)#to_string + (elt#getAttributeNS ~namespaceURI:xlink_ns + ~localName)#to_string gdk_button else ignore (self#action_toggle elt)); @@ -231,7 +249,7 @@ object (self) ignore (self#coerce#misc#grab_selection Gdk.Atom.primary) in let rec aux elt = - if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns + if (elt#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds)#to_string <> "" then set_selection elt @@ -243,7 +261,7 @@ object (self) with GdomeInit.DOMCastException _ -> () in (match gdome_elt with - | Some elt when (elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns + | Some elt when (elt#getAttributeNS ~namespaceURI:xlink_ns ~localName:href_ds)#to_string <> "" -> set_selection elt | Some elt -> aux elt @@ -274,14 +292,14 @@ object (self) (try Hashtbl.find ids_to_terms id with Not_found -> assert false) method private string_of_node node = - if node#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds + if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds then self#string_of_id_node node else string_of_dom_node node method private string_of_id_node node = let get_id (node: Gdome.element) = let xref_attr = - node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds + node#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds in List.hd (HExtlib.split ~sep:' ' xref_attr#to_string) in @@ -369,7 +387,7 @@ object (self) Hashtbl.create 1, None)); let name = "sequent_viewer.xml" in MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name); - ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); + ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement method load_object obj = @@ -389,7 +407,7 @@ object (self) | _ -> let name = "cic_browser.xml" in MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name); - ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); + ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml); end @@ -519,7 +537,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = let markup = match depth, pos with | 0, _ -> `Current (render_switch sw) - | 1, pos when Stack.head_tag stack = Stack.BranchTag -> + | 1, pos when Stack.head_tag stack = `BranchTag -> `Shift (pos, render_switch sw) | _ -> render_switch sw in @@ -538,7 +556,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = (match goal_switch with | Stack.Open goal -> cicMathView#load_sequent _metasenv goal | Stack.Closed goal -> - let doc = Lazy.force MatitaMisc.closed_goal_mathml in + let doc = Lazy.force closed_goal_mathml in cicMathView#load_root ~root:doc#get_documentElement); (try cicMathView#set_selection None; @@ -775,8 +793,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private blank () = self#_showMath; - mathView#load_root - (Lazy.force MatitaMisc.empty_mathml)#get_documentElement + mathView#load_root (Lazy.force empty_mathml)#get_documentElement method private _loadCheck term = failwith "not implemented _loadCheck"; diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 17473f38b..e311973c9 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -38,39 +38,6 @@ let baseuri_of_baseuri_decl st = Some buri | _ -> None -let baseuri_of_file file = - let uri = ref None in - let ic = open_in file in - let istream = Ulexing.from_utf8_channel ic in - (try - while true do - try - let stm = GrafiteParser.parse_statement istream in - match baseuri_of_baseuri_decl stm with - | Some buri -> - let u = strip_trailing_slash buri in - if String.length u < 5 || String.sub u 0 5 <> "cic:/" then - MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri); - (try - ignore(Http_getter.resolve u) - with - | Http_getter_types.Unresolvable_URI _ -> - MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri) - | Http_getter_types.Key_not_found _ -> ()); - uri := Some u; - raise End_of_file - | None -> () - with - CicNotationParser.Parse_error _ as exn -> - prerr_endline ("Unable to parse: " ^ file); - prerr_endline (MatitaExcPp.to_string exn); - () - done - with End_of_file -> close_in ic); - match !uri with - | Some uri -> uri - | None -> failwith ("No baseuri defined in " ^ file) - let is_empty buri = List.for_all (function @@ -115,17 +82,6 @@ let append_phrase_sep s = else s -let empty_mathml = lazy ( - DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns) - ~qualifiedName:(Gdome.domString "math") ~doctype:None) - -let empty_boxml = lazy ( - DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) - ~qualifiedName:(Gdome.domString "box") ~doctype:None) - -let closed_goal_mathml = lazy ( - DomMisc.domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ()) - exception History_failure type 'a memento = 'a array * int * int * int (* data, hd, tl, cur *) @@ -220,50 +176,6 @@ let singleton f = let instance = lazy (f ()) in fun () -> Lazy.force instance -let get_current_proof status = - match status.proof_status with - | Incomplete_proof { proof = p } -> p - | _ -> statement_error "no ongoing proof" - -let get_proof_metasenv status = - match status.proof_status with - | No_proof -> [] - | Proof (_, metasenv, _, _) - | Incomplete_proof { proof = (_, metasenv, _, _) } - | Intermediate metasenv -> - metasenv - -let get_proof_context status goal = - match status.proof_status with - | Incomplete_proof { proof = (_, metasenv, _, _) } -> - let (_, context, _) = CicUtil.lookup_meta goal metasenv in - context - | _ -> [] - -let get_proof_conclusion status goal = - match status.proof_status with - | Incomplete_proof { proof = (_, metasenv, _, _) } -> - let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in - conclusion - | _ -> statement_error "no ongoing proof" - -let get_stack status = - match status.proof_status with - | Incomplete_proof p -> p.stack - | Proof _ -> Continuationals.Stack.empty - | _ -> assert false - -let set_stack stack status = - match status.proof_status with - | Incomplete_proof p -> - { status with proof_status = Incomplete_proof { p with stack = stack } } - | Proof _ -> - assert (Continuationals.Stack.is_empty stack); - status - | _ -> assert false - -let qualify status name = get_string_option status "baseuri" ^ "/" ^ name - let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n let end_ma_RE = Pcre.regexp "\\.ma$" @@ -275,11 +187,6 @@ let obj_file_of_baseuri baseuri = in path ^ ".moo" -let obj_file_of_script f = - if f = "coq.ma" then BuildTimeConf.coq_notation_script else - let baseuri = baseuri_of_file f in - obj_file_of_baseuri baseuri - let list_tl_at ?(equality=(==)) e l = let rec aux = function diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 8dbde7fd9..a04258aee 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -23,8 +23,6 @@ * http://helm.cs.unibo.it/ *) -val baseuri_of_file : string -> string - val baseuri_of_baseuri_decl: ('a, 'b, 'c, 'd, 'e) GrafiteAst.statement -> string option @@ -61,14 +59,6 @@ val strip_suffix: suffix:string -> string -> string * @raise Not_found *) val list_tl_at: ?equality:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list - (** Gdome.element of a MathML document whose rendering should be blank. Used - * by cicBrowser to render "about:blank" document *) -val empty_mathml: Gdome.document lazy_t -val empty_boxml: Gdome.document lazy_t - - (** shown for goals closed by side effects *) -val closed_goal_mathml: Gdome.document lazy_t - exception History_failure type 'a memento @@ -97,21 +87,7 @@ class ['a] browser_history: ?memento:'a memento -> int -> 'a -> ['a] history * first time it gets called. Next invocation will return first value *) val singleton: (unit -> 'a) -> (unit -> 'a) -val qualify: MatitaTypes.status -> string -> string - -val get_current_proof: MatitaTypes.status -> ProofEngineTypes.proof -val get_stack: MatitaTypes.status -> Continuationals.Stack.t -val set_stack: Continuationals.Stack.t ->MatitaTypes.status ->MatitaTypes.status -val get_proof_metasenv: MatitaTypes.status -> Cic.metasenv - -val get_proof_context: - MatitaTypes.status -> ProofEngineTypes.goal -> Cic.context - -val get_proof_conclusion: - MatitaTypes.status -> ProofEngineTypes.goal -> Cic.term - (** given the base name of an image, returns its full path *) val image_path: string -> string val obj_file_of_baseuri: string -> string -val obj_file_of_script: string -> string diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 080450416..bd707de1e 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -214,8 +214,8 @@ let eval_with_engine guistuff status user_goal parsed_text st = let disambiguate_macro_term term status user_goal = let module MD = MatitaDisambiguator in let dbd = MatitaDb.instance () in - let metasenv = MatitaMisc.get_proof_metasenv status in - let context = MatitaMisc.get_proof_context status user_goal in + let metasenv = MatitaTypes.get_proof_metasenv status in + let context = MatitaTypes.get_proof_context status user_goal in let interps = MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases ~universe:(Some status.multi_aliases) term in @@ -276,7 +276,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = [], parsed_text_length (* REAL macro *) | TA.Hint loc -> - let proof = MatitaMisc.get_current_proof status in + let proof = MatitaTypes.get_current_proof status in let proof_status = proof, user_goal in let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in let selected = guistuff.urichooser l in @@ -304,8 +304,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = ) selected; assert false) | TA.Check (_,term) -> - let metasenv = MatitaMisc.get_proof_metasenv status in - let context = MatitaMisc.get_proof_context status user_goal in + let metasenv = MatitaTypes.get_proof_metasenv status in + let context = MatitaTypes.get_proof_context status user_goal in let interps = MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases ~universe:(Some status.multi_aliases) term @@ -759,11 +759,11 @@ object (self) | Incomplete_proof _ -> true | Intermediate _ -> assert false -(* method proofStatus = MatitaMisc.get_proof_status self#status *) - method proofMetasenv = MatitaMisc.get_proof_metasenv self#status - method proofContext = MatitaMisc.get_proof_context self#status userGoal - method proofConclusion = MatitaMisc.get_proof_conclusion self#status userGoal - method stack = MatitaMisc.get_stack self#status +(* method proofStatus = MatitaTypes.get_proof_status self#status *) + method proofMetasenv = MatitaTypes.get_proof_metasenv self#status + method proofContext = MatitaTypes.get_proof_context self#status userGoal + method proofConclusion = MatitaTypes.get_proof_conclusion self#status userGoal + method stack = MatitaTypes.get_stack self#status method setGoal n = userGoal <- n method goal = userGoal diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 29fefca03..df21e09f4 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -89,8 +89,6 @@ let set_metasenv metasenv status = let dump_status status = MatitaLog.message "status.aliases:\n"; - MatitaLog.message - (DisambiguatePp.pp_environment status.aliases ^ "\n"); MatitaLog.message "status.proof_status:"; MatitaLog.message (match status.proof_status with @@ -246,3 +244,47 @@ class type mathViewer = ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit end +let qualify status name = get_string_option status "baseuri" ^ "/" ^ name + +let get_current_proof status = + match status.proof_status with + | Incomplete_proof { proof = p } -> p + | _ -> statement_error "no ongoing proof" + +let get_proof_metasenv status = + match status.proof_status with + | No_proof -> [] + | Proof (_, metasenv, _, _) + | Incomplete_proof { proof = (_, metasenv, _, _) } + | Intermediate metasenv -> + metasenv + +let get_proof_context status goal = + match status.proof_status with + | Incomplete_proof { proof = (_, metasenv, _, _) } -> + let (_, context, _) = CicUtil.lookup_meta goal metasenv in + context + | _ -> [] + +let get_proof_conclusion status goal = + match status.proof_status with + | Incomplete_proof { proof = (_, metasenv, _, _) } -> + let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in + conclusion + | _ -> statement_error "no ongoing proof" + +let get_stack status = + match status.proof_status with + | Incomplete_proof p -> p.stack + | Proof _ -> Continuationals.Stack.empty + | _ -> assert false + +let set_stack stack status = + match status.proof_status with + | Incomplete_proof p -> + { status with proof_status = Incomplete_proof { p with stack = stack } } + | Proof _ -> + assert (Continuationals.Stack.is_empty stack); + status + | _ -> assert false + diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index e425519c6..f27f2a11b 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -114,3 +114,14 @@ class type mathViewer = method show_uri_list : ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit end + +val qualify: status -> string -> string + +val get_current_proof: status -> ProofEngineTypes.proof +val get_proof_metasenv: status -> Cic.metasenv +val get_proof_context: status -> ProofEngineTypes.goal -> Cic.context +val get_proof_conclusion: status -> ProofEngineTypes.goal -> Cic.term +val get_stack: status -> Continuationals.Stack.t + +val set_stack: Continuationals.Stack.t -> status -> status + diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml index 40526e74d..7250492f8 100644 --- a/helm/matita/matitac.ml +++ b/helm/matita/matitac.ml @@ -23,10 +23,15 @@ * http://helm.cs.unibo.it/ *) +let main () = + match Filename.basename Sys.argv.(0) with + | "matitadep" -> Matitadep.main () + | "matitaclean" -> Matitaclean.main () + | "matitamake" -> Matitamake.main () + | _ -> + let _ = Paramodulation.Saturation.init () in (* ALB to link paramodulation *) + let _ = MatitacLib.main `COMPILER in + () -(* ALB to link paramodulation... *) -let _ = Paramodulation.Saturation.init () - - -let _ = MatitacLib.main `COMPILER +let _ = main () diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 413b3b552..8552cbf86 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -182,7 +182,7 @@ let main ~mode = end else begin - let moo_fname = MatitaMisc.obj_file_of_script fname in + let moo_fname = MatitacleanLib.obj_file_of_script fname in MatitaMoo.save_moo moo_fname moo_content_rev; MatitaLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index 9a5d1bf01..5aabf7558 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -28,11 +28,8 @@ open Printf module UM = UriManager module TA = GrafiteAst -let _ = MatitaInit.initialize_all () - -let main = MatitacleanLib.clean_baseuris - -let _ = +let main () = + let _ = MatitaInit.initialize_all () in let uris_to_remove = ref [] in let files_to_remove = ref [] in (match Helm_registry.get_list Helm_registry.string "matita.args" with @@ -57,7 +54,7 @@ let _ = UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> files_to_remove := suri :: !files_to_remove; - let u = MatitaMisc.baseuri_of_file suri in + let u = MatitacleanLib.baseuri_of_file suri in if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin MatitaLog.error (sprintf "File %s defines a bad baseuri: %s" suri u); @@ -67,7 +64,7 @@ let _ = in uris_to_remove := uri :: !uris_to_remove) files); - main !uris_to_remove; - let moos = List.map MatitaMisc.obj_file_of_script !files_to_remove in + MatitacleanLib.clean_baseuris !uris_to_remove; + let moos = List.map MatitacleanLib.obj_file_of_script !files_to_remove in List.iter MatitaMisc.safe_remove moos diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index e8a1fd29a..82fac08af 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/matita/matitacleanLib.ml @@ -227,3 +227,41 @@ let clean_baseuris ?(verbose=true) buris = MetadataTypes.count_tbl()] end +let baseuri_of_file file = + let uri = ref None in + let ic = open_in file in + let istream = Ulexing.from_utf8_channel ic in + (try + while true do + try + let stm = GrafiteParser.parse_statement istream in + match MatitaMisc.baseuri_of_baseuri_decl stm with + | Some buri -> + let u = MatitaMisc.strip_trailing_slash buri in + if String.length u < 5 || String.sub u 0 5 <> "cic:/" then + MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri); + (try + ignore(Http_getter.resolve u) + with + | Http_getter_types.Unresolvable_URI _ -> + MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri) + | Http_getter_types.Key_not_found _ -> ()); + uri := Some u; + raise End_of_file + | None -> () + with + CicNotationParser.Parse_error _ as exn -> + prerr_endline ("Unable to parse: " ^ file); + prerr_endline (MatitaExcPp.to_string exn); + () + done + with End_of_file -> close_in ic); + match !uri with + | Some uri -> uri + | None -> failwith ("No baseuri defined in " ^ file) + +let obj_file_of_script f = + if f = "coq.ma" then BuildTimeConf.coq_notation_script else + let baseuri = baseuri_of_file f in + MatitaMisc.obj_file_of_baseuri baseuri + diff --git a/helm/matita/matitacleanLib.mli b/helm/matita/matitacleanLib.mli index 2d8095fb2..91aa51b2a 100644 --- a/helm/matita/matitacleanLib.mli +++ b/helm/matita/matitacleanLib.mli @@ -25,3 +25,6 @@ val clean_baseuris : ?verbose:bool -> string list -> unit +val baseuri_of_file: string -> string +val obj_file_of_script : string -> string + diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 3eb83af00..5b22cb70b 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -26,36 +26,32 @@ module GA = GrafiteAst module U = UriManager -(* all are maps from "file" to "something" *) -let include_deps = Hashtbl.create (Array.length Sys.argv) -let baseuri_of = Hashtbl.create (Array.length Sys.argv) -let uri_deps = Hashtbl.create (Array.length Sys.argv) - -let buri alias = - U.buri_of_uri (U.uri_of_string alias) - -let resolve alias current_buri= - let buri = buri alias in - if buri <> current_buri then Some buri else None - -let find path = - let rec aux = function - | [] -> close_in (open_in path); path - | p :: tl -> - try - close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path - with Sys_error _ -> aux tl - in - let paths = Helm_registry.get_list Helm_registry.string "matita.includes" in - try - aux paths - with Sys_error _ as exc -> - MatitaLog.error ("Unable to read " ^ path); - MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths); - raise exc -;; - let main () = + (* all are maps from "file" to "something" *) + let include_deps = Hashtbl.create (Array.length Sys.argv) in + let baseuri_of = Hashtbl.create (Array.length Sys.argv) in + let uri_deps = Hashtbl.create (Array.length Sys.argv) in + let buri alias = U.buri_of_uri (U.uri_of_string alias) in + let resolve alias current_buri = + let buri = buri alias in + if buri <> current_buri then Some buri else None + in + let find path = + let rec aux = function + | [] -> close_in (open_in path); path + | p :: tl -> + try + close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path + with Sys_error _ -> aux tl + in + let paths = Helm_registry.get_list Helm_registry.string "matita.includes" in + try + aux paths + with Sys_error _ as exc -> + MatitaLog.error ("Unable to read " ^ path); + MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths); + raise exc + in MatitaInit.load_configuration_file (); MatitaInit.parse_cmdline (); List.iter @@ -75,7 +71,7 @@ let main () = | GrafiteAst.IncludeDep path -> try let ma_file = if path <> "coq.ma" then find path else path in - let moo_file = MatitaMisc.obj_file_of_script ma_file in + let moo_file = MatitacleanLib.obj_file_of_script ma_file in Hashtbl.add include_deps file moo_file with Sys_error _ -> MatitaLog.warn @@ -96,11 +92,8 @@ let main () = let deps = List.fast_sort Pervasives.compare deps in let deps = HExtlib.list_uniq deps in let deps = file :: deps in - let moo = MatitaMisc.obj_file_of_script file in + let moo = MatitacleanLib.obj_file_of_script file in Printf.printf "%s: %s\n" moo (String.concat " " deps); Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo) (Helm_registry.get_list Helm_registry.string "matita.args") -;; - -let _ = - main () + diff --git a/helm/matita/matitamake.ml b/helm/matita/matitamake.ml index b967fee19..46b194bda 100644 --- a/helm/matita/matitamake.ml +++ b/helm/matita/matitamake.ml @@ -25,154 +25,136 @@ module MK = MatitamakeLib ;; -let _ = - MatitaInit.load_configuration_file (); - MK.initialize () -;; - -let usage = ref (fun () -> ()) - -let dev_of_name name = - match MK.development_for_name name with - | None -> - prerr_endline ("Unable to find a development called " ^ name); - exit 1 - | Some d -> d -;; - -let dev_for_dir dir = - match MK.development_for_dir dir with - | None -> - prerr_endline ("Unable to find a development holding directory: " ^ dir); - exit 1 - | Some d -> d -;; - -let init_dev_doc = " +let main () = + Helm_registry.load_from BuildTimeConf.matita_conf; + MK.initialize (); + let usage = ref (fun () -> ()) in + let dev_of_name name = + match MK.development_for_name name with + | None -> + prerr_endline ("Unable to find a development called " ^ name); + exit 1 + | Some d -> d + in + let dev_for_dir dir = + match MK.development_for_dir dir with + | None -> + prerr_endline ("Unable to find a development holding directory: "^ dir); + exit 1 + | Some d -> d + in + let init_dev_doc = " \tParameters: name (the name of the development, required) \tDescription: tells matitamake that a new development radicated \t\tin the current working directory should be handled." -;; - -let init_dev args = - if List.length args <> 1 then !usage (); - match MK.initialize_development (List.hd args) (Unix.getcwd ()) with - | None -> exit 2 - | Some _ -> exit 0 -;; - -let list_dev_doc = " + in + let init_dev args = + if List.length args <> 1 then !usage (); + match MK.initialize_development (List.hd args) (Unix.getcwd ()) with + | None -> exit 2 + | Some _ -> exit 0 + in + let list_dev_doc = " \tParameters: \tDescription: lists the known developments and their roots." -;; - -let list_dev args = - if List.length args <> 0 then !usage (); - match MK.list_known_developments () with - | [] -> print_string "No developments found.\n"; exit 0 - | l -> - List.iter - (fun (name, root) -> - print_string (Printf.sprintf "%-10s\trooted in %s\n" name root)) - l; - exit 0 -;; - -let destroy_dev_doc = " + in + let list_dev args = + if List.length args <> 0 then !usage (); + match MK.list_known_developments () with + | [] -> print_string "No developments found.\n"; exit 0 + | l -> + List.iter + (fun (name, root) -> + print_string (Printf.sprintf "%-10s\trooted in %s\n" name root)) + l; + exit 0 + in + let destroy_dev_doc = " \tParameters: name (the name of the development to destroy, required) \tDescription: deletes a development (only from matitamake metadat, no \t\t.ma files will be deleted)." - -let destroy_dev args = - if List.length args <> 1 then !usage (); - let name = (List.hd args) in - let dev = dev_of_name name in - MK.destroy_development dev; - exit 0 -;; - -let clean_dev_doc = " + in + let destroy_dev args = + if List.length args <> 1 then !usage (); + let name = (List.hd args) in + let dev = dev_of_name name in + MK.destroy_development dev; + exit 0 + in + let clean_dev_doc = " \tParameters: name (the name of the development to destroy, optional) \t\tIf omitted the development that holds the current working \t\tdirectory is used (if any). \tDescription: clean the develpoment." - -let clean_dev args = - let dev = - match args with - | [] -> dev_for_dir (Unix.getcwd ()) - | [name] -> dev_of_name name - | _ -> !usage (); exit 1 - in - match MK.clean_development dev with - | true -> exit 0 - | false -> exit 1 -;; - -let build_dev_doc = " + in + let clean_dev args = + let dev = + match args with + | [] -> dev_for_dir (Unix.getcwd ()) + | [name] -> dev_of_name name + | _ -> !usage (); exit 1 + in + match MK.clean_development dev with + | true -> exit 0 + | false -> exit 1 + in + let build_dev_doc = " \tParameters: name (the name of the development to build, required) \tDescription: completely builds the develpoment." - -let build_dev args = - if List.length args <> 1 then !usage (); - let name = (List.hd args) in - let dev = dev_of_name name in - match MK.build_development dev with - | true -> exit 0 - | false -> exit 1 -;; - -let nodb_doc = " + in + let build_dev args = + if List.length args <> 1 then !usage (); + let name = (List.hd args) in + let dev = dev_of_name name in + match MK.build_development dev with + | true -> exit 0 + | false -> exit 1 + in + let nodb_doc = " \tParameters: \tDescription: avoid using external database connection." - -let nodb _ = Helm_registry.set_bool "db.nodb" true - -let target args = - if List.length args < 1 then !usage (); - let dev = dev_for_dir (Unix.getcwd ()) in - List.iter - (fun t -> - ignore(MK.build_development ~target:t dev)) - args -;; - -let params = [ - "-init", init_dev, init_dev_doc; - "-clean", clean_dev, clean_dev_doc; - "-list", list_dev, list_dev_doc; - "-destroy", destroy_dev, destroy_dev_doc; - "-build", build_dev, build_dev_doc; - "-nodb", nodb, nodb_doc; - "-h", (fun _ -> !usage()), "print this help screen"; - "-help", (fun _ -> !usage()), "print this help screen"; -] -;; - -usage := fun () -> - let p = prerr_endline in - p "\nusage:"; - p "\tmatitamake(.opt) [command [options]]\n"; - p "\tmatitamake(.opt) [target]\n"; - p "commands:"; - List.iter (fun (n,_,d) -> p (Printf.sprintf " %-10s%s" n d)) params; - p "\nIf target is omitted a 'all' will be used as the default."; - p "With -build you can build a development wherever it is."; - p "If you specify a target it implicitly refers to the development that"; - p "holds the current working directory (if any).\n"; - exit 1 -;; - -let rec parse args = - match args with - | [] -> target ["all"] - | s::tl -> - try - let _,f,_ = List.find (fun (n,_,_) -> n = s) params in - f tl; - parse tl - with Not_found -> if s.[0] = '-' then !usage () else target args - -let _ = + in + let nodb _ = Helm_registry.set_bool "db.nodb" true in + let target args = + if List.length args < 1 then !usage (); + let dev = dev_for_dir (Unix.getcwd ()) in + List.iter + (fun t -> + ignore(MK.build_development ~target:t dev)) + args + in + let params = [ + "-init", init_dev, init_dev_doc; + "-clean", clean_dev, clean_dev_doc; + "-list", list_dev, list_dev_doc; + "-destroy", destroy_dev, destroy_dev_doc; + "-build", build_dev, build_dev_doc; + "-nodb", nodb, nodb_doc; + "-h", (fun _ -> !usage()), "print this help screen"; + "-help", (fun _ -> !usage()), "print this help screen"; + ] + in + usage := (fun () -> + let p = prerr_endline in + p "\nusage:"; + p "\tmatitamake(.opt) [command [options]]\n"; + p "\tmatitamake(.opt) [target]\n"; + p "commands:"; + List.iter (fun (n,_,d) -> p (Printf.sprintf " %-10s%s" n d)) params; + p "\nIf target is omitted a 'all' will be used as the default."; + p "With -build you can build a development wherever it is."; + p "If you specify a target it implicitly refers to the development that"; + p "holds the current working directory (if any).\n"; + exit 1); + let rec parse args = + match args with + | [] -> target ["all"] + | s::tl -> + try + let _,f,_ = List.find (fun (n,_,_) -> n = s) params in + f tl; + parse tl + with Not_found -> if s.[0] = '-' then !usage () else target args + in parse (List.tl (Array.to_list Sys.argv)) - +