]> matita.cs.unibo.it Git - helm.git/commitdiff
better dependencies among modules and symlinking of several matitatools to a single...
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 3 Nov 2005 15:00:47 +0000 (15:00 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 3 Nov 2005 15:00:47 +0000 (15:00 +0000)
25 files changed:
helm/matita/.cvsignore
helm/matita/.depend
helm/matita/Makefile.in
helm/matita/configure.ac
helm/matita/matita.glade
helm/matita/matita.ml
helm/matita/matitaEngine.ml
helm/matita/matitaGtkMisc.ml
helm/matita/matitaGtkMisc.mli
helm/matita/matitaGui.ml
helm/matita/matitaGuiTypes.mli
helm/matita/matitaInit.ml
helm/matita/matitaMathView.ml
helm/matita/matitaMisc.ml
helm/matita/matitaMisc.mli
helm/matita/matitaScript.ml
helm/matita/matitaTypes.ml
helm/matita/matitaTypes.mli
helm/matita/matitac.ml
helm/matita/matitacLib.ml
helm/matita/matitaclean.ml
helm/matita/matitacleanLib.ml
helm/matita/matitacleanLib.mli
helm/matita/matitadep.ml
helm/matita/matitamake.ml

index babd18569d60703709fc34befe6795ed3007fcea..db41158dead619952d1ecd8eb138f0bca6278480 100644 (file)
@@ -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
index d4bad940454f8d32c8e5d47e2f32b05a59e8cb72..f6d37dcf8522809e820b06c00a02f4e761840dec 100644 (file)
@@ -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 
index c1e1c094e95ea938a6476d348ede3261201b62a6..b1239778ca42248d6889c1d0b192de68f0ffd1fc 100644 (file)
@@ -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
index 012b547932e4bd888abc459af08081134509a4cf..4f8c991d1082d380e1fd4fe6bdcd089360e5d87e 100644 (file)
@@ -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)
index ecb2e4061db468378239a7f49160266bcf44037d..3c664c43cc7505077d2d73d2f1b94e14e5fe3266 100644 (file)
   </child>
 </widget>
 
-<widget class="GtkDialog" id="InterpChoiceDialog">
+<widget class="GtkDialog" id="RecordChoiceDialog">
   <property name="width_request">350</property>
   <property name="height_request">250</property>
-  <property name="title" translatable="yes">Interpretation choice</property>
+  <property name="title" translatable="yes">title</property>
   <property name="type">GTK_WINDOW_TOPLEVEL</property>
   <property name="window_position">GTK_WIN_POS_NONE</property>
   <property name="modal">True</property>
          <property name="layout_style">GTK_BUTTONBOX_END</property>
 
          <child>
-           <widget class="GtkButton" id="InterpChoiceHelpButton">
+           <widget class="GtkButton" id="RecordChoiceHelpButton">
              <property name="visible">True</property>
              <property name="can_default">True</property>
              <property name="can_focus">True</property>
          </child>
 
          <child>
-           <widget class="GtkButton" id="InterpChoiceCancelButton">
+           <widget class="GtkButton" id="RecordChoiceCancelButton">
              <property name="visible">True</property>
              <property name="can_default">True</property>
              <property name="can_focus">True</property>
          </child>
 
          <child>
-           <widget class="GtkButton" id="InterpChoiceOkButton">
+           <widget class="GtkButton" id="RecordChoiceOkButton">
              <property name="visible">True</property>
              <property name="can_default">True</property>
              <property name="can_focus">True</property>
          <property name="spacing">0</property>
 
          <child>
-           <widget class="GtkLabel" id="InterpChoiceDialogLabel">
+           <widget class="GtkLabel" id="RecordChoiceDialogLabel">
              <property name="visible">True</property>
              <property name="label" translatable="yes">some informative message here ...</property>
              <property name="use_underline">False</property>
              <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 
              <child>
-               <widget class="GtkTreeView" id="InterpChoiceTreeView">
+               <widget class="GtkTreeView" id="RecordChoiceTreeView">
                  <property name="visible">True</property>
                  <property name="can_focus">True</property>
                  <property name="headers_visible">False</property>
index b9e09f24d8dbc88bcbbaa4ca05c4ca30dc71e4c7..dd8d6d83dad6a115d6e13540a44fc128ca8c0cb7 100644 (file)
@@ -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
index 9595df9317714358a1de9e3f1a0f3fbedc0959db..1d3b1f94e0d74c58525610eca3894e4e9bb46363 100644 (file)
@@ -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
index 0ad36dfee8f5e04fd3d255b42e6dc8ee0adaadb8..3c0d1b4c359ba15ba418b70f1cd74585a6d27484 100644 (file)
@@ -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)
+
index e5d0e9be907a3c5be75673ba7d8b37f82590ec79..1affd2a39e78822d2449ef7abe087d57102b4717 100644 (file)
@@ -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
+
index bf25a5493a75ba8eb0764a9d8ffb6ee32d963d3b..d4157677feabd3573bae00edf5c4d84d52795c3d 100644 (file)
@@ -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)
 
index cf738cd85caa501f8fa103a4ac552956f4ffb781..99b90495f15de3eb0fdbecc5d9079989fe68c020 100644 (file)
@@ -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
 
index e69c22cf87a7897f36c1c071df9c6e4c221a37d0..9ea9e07d2670d89729b3b9fe5eafbbc9487a928f 100644 (file)
@@ -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
index 1ad4b2cd10a79dd14348b67d157d4b4b7552beab..f9c617385a945e8a4facc9ee39517f6816729fc6 100644 (file)
@@ -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";
index 17473f38b3826029c62674fa7e8a6e23371ab928..e311973c9cc362c726d503839154c2efee644c0b 100644 (file)
@@ -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
index 8dbde7fd9f0308731380615cb29216341c1878c5..a04258aee771bb6e63898a9d3fb3d279d2c7e978 100644 (file)
@@ -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
 
index 080450416feacdcb27e5b62bdf6c8caf7ca80111..bd707de1eb522af2e148afc198a2ad464e685732 100644 (file)
@@ -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
 
index 29fefca03f9563a86975f4e317e17da9e8bfe05b..df21e09f44583c58c22db32f729f8a73765451c2 100644 (file)
@@ -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
index e425519c6434242d593619175c85a34fb89c8156..f27f2a11ba69fbc7bc74eeebced9db4fe5a528c6 100644 (file)
@@ -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
+
index 40526e74d4a4a59eed02f77f14bc5492ee526ddd..7250492f835ce753696f741ee7be89a3b959d120 100644 (file)
  * 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 ()
 
index 413b3b5521d2ac35bc9eaf2b476efbb2ca42aed9..8552cbf8629ba98f72086fd58c11d67512bd9d49 100644 (file)
@@ -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));
index 9a5d1bf018228a995ad8a9a48d3d817dae32f1cc..5aabf7558dab32467027798a40446199f0fc3646 100644 (file)
@@ -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
 
index e8a1fd29a301bf1141f4ae2739929664aa2f9426..82fac08af78a1a7516719a9ab78733be4e1e8e5d 100644 (file)
@@ -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
+
index 2d8095fb2d70acd780d0b32afc85a68af160ddc9..91aa51b2a1350094aa840e35fba3baeeb7c544a2 100644 (file)
@@ -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
+
index 3eb83af00964690ebf276127c9fa44f3e1a412c3..5b22cb70b9cbe9abce580c4d254a0344b009a3d4 100644 (file)
 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 ()
+
index b967fee19e530d39431fe06cc83ae44e7058cd90..46b194bda7126bb207cd58f66a88565919e4a879 100644 (file)
 
 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))
-  
+