From: Claudio Sacerdoti Coen Date: Tue, 3 Jan 2023 17:59:47 +0000 (+0100) Subject: Remove all traces of autoconf/automake/makefile X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0d6b83167358b4015beea961f79c577f9ff0d88d;p=helm.git Remove all traces of autoconf/automake/makefile - also fixes installation of help/C files to include only .xml files and figures --- diff --git a/.gitignore b/.gitignore index 7ad5d443d..d2e1e23e5 100644 --- a/.gitignore +++ b/.gitignore @@ -20,7 +20,6 @@ matita/config.log matita/configure matita/components/extlib/componentsConf.ml -matita/matita/matitaGeneratedGui.ml matita/matita/matita.conf.xml matita/matita/matita.glade.utf8 matita/depend-stamp diff --git a/matita/.merlin b/matita/.merlin deleted file mode 100644 index 92f60a69a..000000000 --- a/matita/.merlin +++ /dev/null @@ -1,9 +0,0 @@ -S components/* -S matita - -B components/* -B matita - -PKG lablgtk3 helm-content helm-ng_disambiguation helm-content_pres helm-ng_extraction helm-disambiguation helm-ng_kernel helm-extlib helm-ng_library helm-getter helm-ng_paramodulation helm-grafite helm-ng_refiner helm-grafite_engine helm-ng_tactics helm-grafite_parser helm-registry helm-library helm-syntax_extensions helm-logger helm-thread helm-ng_cic_content helm-xml - -FLG -rectypes diff --git a/matita/Makefile b/matita/Makefile deleted file mode 100644 index 208091758..000000000 --- a/matita/Makefile +++ /dev/null @@ -1,127 +0,0 @@ -H=@ - -include Makefile.defs - -SUBDIRS = components matita - -ifeq ($(DISTRIBUTED),yes) -# 'world' is the default target when distributed, otherwise 'all' is -world: depend $(foreach d,$(SUBDIRS),rec@world@$(d)) -all: depend $(foreach d,$(SUBDIRS),rec@all@$(d)) -opt: depend $(foreach d,$(SUBDIRS),rec@opt@$(d)) -else -all: $(foreach d,$(SUBDIRS),rec@all@$(d)) -opt: $(foreach d,$(SUBDIRS),rec@opt@$(d)) -world: depend $(foreach d,$(SUBDIRS),rec@world@$(d)) -endif -depend: depend-stamp -depend-stamp: -ifeq ($(HAVE_OCAMLOPT),yes) - ifeq ($(DISTRIBUTED),yes) - $(MAKE) $(foreach d,$(SUBDIRS),rec@depend.opt@$(d)) - else - $(MAKE) $(foreach d,$(SUBDIRS),rec@depend@$(d)) - endif -else - $(MAKE) $(foreach d,$(SUBDIRS),rec@depend@$(d)) -endif - $(H)touch depend-stamp - -clean: - $(H)make $(foreach d,$(SUBDIRS),rec@clean@$(d)) || true -distclean: - $(H)make $(foreach d,$(SUBDIRS),rec@distclean@$(d)) || true - $(H)rm -rf .matita library-stamp depend-stamp -install-indep: $(foreach d,$(SUBDIRS),rec@install-indep@$(d)) -install-arch: $(foreach d,$(SUBDIRS),rec@install-arch@$(d)) -install: install-indep install-arch -uninstall: $(foreach d,$(SUBDIRS),rec@uninstall@$(d)) - -rec@%: - $(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*)) DESTDIR=$(DESTDIR) - -# {{{ Distribution stuff - -ifeq ($(DISTRIBUTED),yes) -library: library-stamp -library-stamp: - $(MAKE) -C matita/ dist_library - touch $@ -endif - -BASENAME = matita -NULL = -DISTDIR = $(BASENAME)-$(MATITA_VERSION) -CLEAN_ON_DIST = \ - components/license \ - matita/TPTP/ \ - matita/contribs/ \ - components/binaries/matitaprover/benchmarks/ \ - matita/library/ \ - matita/nlibrary/ \ - matita/scripts/ \ - matita/tests/ \ - matita/lib/lambdaN/ \ - matita/lib/lambda/ \ - $(NULL) -EXTRA_DIST = \ - matita/AUTHORS \ - matita/LICENSE \ - matita/dist/BUGS \ - matita/dist/ChangeLog \ - matita/dist/COPYING \ - Makefile \ - Makefile.defs.in \ - $(NULL) -EXTRA_DIST_matita = \ - matita/matitaGeneratedGui.ml \ - $(NULL) - -distcheck: dist dist_extract dist_test - -dist: dist_mktmpdir dist_pre dist_export dist_mktarball dist_rmtmpdir -dist/configure.ac: configure.ac matita/dist/configure.ac.sed - sed -f matita/dist/configure.ac.sed < $< > $@ -dist/configure: dist/configure.ac - cd dist && autoconf -dist_mktmpdir: - test -d dist || mkdir dist -dist_rmtmpdir: - test -d dist && rm -rf dist/ || true -dist_pre: - $(MAKE) -C matita dist_pre -dist_export: dist/configure - rm -rf $(DISTDIR) - mkdir $(DISTDIR) - git archive matita-lablgtk3 components | tar -x -C $(DISTDIR) - git archive matita-lablgtk3 matita | tar -x -C $(DISTDIR) - (cd $(DISTDIR) && find . -name .depend -exec rm \{\} \;) - (cd $(DISTDIR) && find . -name .depend.opt -exec rm \{\} \;) - (cd $(DISTDIR) && rm -rf $(CLEAN_ON_DIST)) - cp $< $(DISTDIR)/configure - cp dist/configure.ac $(DISTDIR)/configure.ac - cp -r $(EXTRA_DIST) $(DISTDIR) - cp -r $(EXTRA_DIST_matita) $(DISTDIR)/matita - # distribute HTML version of the manual - mkdir -p $(DISTDIR)/docs/manual/ - $(MAKE) -C matita/help/C/ install DESTDIR=$(CURDIR)/$(DISTDIR)/docs/manual/ -dist_mktarball: - tar czf $(DISTDIR).tar.gz $(DISTDIR) - #tar cjf $(DISTDIR).tar.bz2 $(DISTDIR) - rm -rf $(DISTDIR) - -dist_extract: - tar xzf $(DISTDIR).tar.gz -dist_test: - (cd $(DISTDIR)/ \ - && ./configure \ - && $(MAKE) world \ - && $(MAKE) install DESTDIR=`pwd`/install) - -.PHONY: dist dist_export dist_mktarball distcheck dist_extract dist_test dist_autotools - -# }}} End of distribution stuff - -.PHONY: all opt clean distclean - -# vim: set foldmethod=marker: diff --git a/matita/Makefile.defs.in b/matita/Makefile.defs.in deleted file mode 100644 index 90a203f73..000000000 --- a/matita/Makefile.defs.in +++ /dev/null @@ -1,16 +0,0 @@ -OCAMLPATH := @OCAMLPATH@:$(OCAMLPATH) -OCAMLFIND = OCAMLPATH=$(OCAMLPATH) @OCAMLFIND@ -CAMLP5O = @CAMLP5O@ -LABLGLADECC = @LABLGLADECC@ -HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ -DISTRIBUTED = @DISTRIBUTED@ -ANNOT = @ANNOT@ - -MATITA_REQUIRES = @FINDLIB_REQUIRES@ -MATITA_CREQUIRES = @FINDLIB_CREQUIRES@ - -MATITA_VERSION = @MATITA_VERSION@ - -SRCROOT = @SRCROOT@ -RT_BASE_DIR = @RT_BASE_DIR@ -DBHOST = @DBHOST@ diff --git a/matita/components/Makefile b/matita/components/Makefile deleted file mode 100644 index f30f28434..000000000 --- a/matita/components/Makefile +++ /dev/null @@ -1,142 +0,0 @@ -H=@ -export SHELL=/bin/bash - -include ../Makefile.defs - -# Warning: the modules must be in compilation order -NULL = -MODULES = \ - extlib \ - xml \ - registry \ - syntax_extensions \ - thread \ - logger \ - ng_kernel \ - ng_extraction \ - getter \ - library \ - content \ - grafite \ - ng_refiner \ - ng_library \ - ng_cic_content \ - disambiguation \ - ng_disambiguation \ - ng_paramodulation \ - content_pres \ - grafite_parser \ - ng_tactics \ - grafite_engine \ - $(NULL) - -METAS = $(MODULES:%=METAS/META.helm-%) - -ifeq ($(DISTRIBUTED),no) - MODULES+=binaries -endif - -all: metas $(MODULES:%=rec@all@%) -opt: metas syntax-extensions $(MODULES:%=rec@opt@%) - -ifeq ($(HAVE_OCAMLOPT),yes) -world: opt -else -world: all -endif -syntax-extensions: - $(H)$(MAKE) -C syntax_extensions depend - $(H)$(MAKE) -C syntax_extensions -depend: syntax-extensions $(MODULES:%=rec@depend@%) -depend.opt: syntax-extensions $(MODULES:%=rec@depend.opt@%) -install-arch: $(MODULES:%=rec@install@%) -install-indep: -uninstall: $(MODULES:%=rec@uninstall@%) -clean: $(MODULES:%=rec@clean@%) clean_metas - -.stats: $(MODULES:%=rec@.stats@%) - $(H)(for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \ - | sort -t : -k 2 -n -r > .stats - -rec@%: - $(H)$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*)) - -EXTRA_DIST_CLEAN = \ - libraries-clusters.ps \ - libraries-clusters.pdf \ - libraries-ext.ps \ - libraries.ps \ - .dep.dot \ - .extdep.dot \ - .clustersdep.dot \ - $(NULL) - -distclean: clean clean_metas - $(H)rm -f $(METAS) - $(H)rm -f configure config.log config.cache config.status - $(H)rm -f $(EXTRA_DIST_CLEAN) - -.PHONY: all opt world metas depend install uninstall clean clean_metas distclean - -METAS/META.helm-%: METAS/meta.helm-%.src - $(H)cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@ - -SIMPLIFYDEPS = ../daemons/graphs/tools/simplify_deps/simplify_deps -$(SIMPLIFYDEPS): - $(H)$(MAKE) -C $(dir $(SIMPLIFYDEPS)) - -.PHONY: .dep.dot -.dep.dot: $(SIMPLIFYDEPS) - $(H)echo "digraph G {" > $@ - $(H)echo " rankdir = TB ;" >> $@ - $(H)for i in $(MODULES); do \ - $(OCAMLFIND) query helm-$$i -recursive -p-format | \ - grep helm | \ - sed "s/^helm-/ \"$$i\" -> \"/g" | \ - sed "s/$$/\";/g" >> $@ ; \ - done - $(H)mv $@ $@.old ; $(SIMPLIFYDEPS) < $@.old > $@ ; rm $@.old - $(H)echo "}" >> $@ - -.PHONY: .alldep.dot -.alldep.dot: - $(H)echo "digraph G {" > $@ - $(H)echo " rankdir = TB ;" >> $@ - $(H)for i in $(MODULES); do \ - $(OCAMLFIND) query helm-$$i -recursive -p-format | \ - grep -v "pxp-" | \ - sed "s/^pxp/pxp[-*]/g" | \ - sed "s/^/ \"helm-$$i\" -> \"/g" | \ - sed "s/$$/\";/g" >> $@ ; \ - done - $(H)mv $@ $@.old ; \ - ./simplify_deps/simplify_deps.opt < $@.old > $@ ; \ - rm $@.old - $(H)for i in $(MODULES); do \ - echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];"\ - >> $@ ; \ - done - $(H)echo "}" >> $@ - -.extdep.dot: .dep.dot - $(H)STATS/patch_deps.sh $< $@ -.clustersdep.dot: .dep.dot - $(H)USE_CLUSTERS=yes STATS/patch_deps.sh $< $@ - -libraries.ps: .dep.dot - $(H)dot -Tps -o $@ $< -libraries-ext.ps: .extdep.dot - $(H)dot -Tps -o $@ $< -libraries-clusters.ps: .clustersdep.dot - $(H)dot -Tps -o $@ $< -libraries-complete.ps: .alldep.dot - $(H)dot -Tps -o $@ $< - -ps: libraries.ps libraries-ext.ps libraries-clusters.ps - -tags: TAGS -.PHONY: TAGS -TAGS: - $(H)otags -vi -r . - -metas: $(filter-out METAS/META.helm-binaries, $(METAS)) diff --git a/matita/components/Makefile.common b/matita/components/Makefile.common deleted file mode 100644 index 0c61faaf7..000000000 --- a/matita/components/Makefile.common +++ /dev/null @@ -1,155 +0,0 @@ -H=@ - -# This Makefile must be included by another one defining: -# $PACKAGE -# $PREDICATES -# $INTERFACE_FILES -# $IMPLEMENTATION_FILES -# $EXTRA_OBJECTS_TO_INSTALL -# $EXTRA_OBJECTS_TO_CLEAN -# and put in a directory where there is a .depend or .depend.opt file. - -# $OCAMLFIND must be set to a meaningful vaule, including OCAMLPATH= - -ifeq ($(ANNOT),true) - ANNOTOPTION = -dtypes -else - ANNOTOPTION = -endif - -PREPROCOPTIONS = -pp camlp5o -SYNTAXOPTIONS = -syntax camlp5o -PREREQ = -OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70 # -57-3 for ocaml 4.0.5, -68-69-70 for ocaml 5.0 -OCAMLDEBUGOPTIONS = -g -#OCAML_PROF=p -p a -OCAMLARCHIVEOPTIONS = -REQUIRES := $(shell $(OCAMLFIND) -query -format '%(requires)' helm-$(PACKAGE)) -OCAMLC = $(OCAMLFIND) ocamlc$(OCAML_PROF) $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(PREPROCOPTIONS) -#OCAMLOPT_DEBUG_FLAGS = -p -OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(PREPROCOPTIONS) $(OCAMLOPT_DEBUG_FLAGS) -OCAMLDEP = $(OCAMLFIND) ocamldep -package "camlp5 $(CAMLP5REQUIRES)" $(SYNTAXOPTIONS) $(OCAMLDEPOPTIONS) -OCAMLLEX = ocamllex -OCAMLYACC = ocamlyacc - -OCAMLC_P4 = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(SYNTAXOPTIONS) -OCAMLOPT_P4 = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(SYNTAXOPTIONS) - -LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -LIBRARIES_DEPS := \ - $(foreach X,$(filter-out /usr/lib/ocaml%,$(LIBRARIES)),\ - $(wildcard \ - $(shell dirname $(X))/*.mli \ - $(shell dirname $(X))/*.ml \ - $(shell dirname $(X))/paramodulation/*.ml \ - $(shell dirname $(X))/paramodultation/*.mli)) - - -ARCHIVE = $(PACKAGE).cma -ARCHIVE_OPT = $(PACKAGE).cmxa -OBJECTS_TO_INSTALL = $(ARCHIVE) $(ARCHIVE_OPT) $(ARCHIVE_OPT:%.cmxa=%.a) \ - $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.cmi) \ - $(EXTRA_OBJECTS_TO_INSTALL) -DEPEND_FILES = $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) - -$(ARCHIVE): $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(LIBRARIES) - $(H)if [ $(PACKAGE) != dummy ]; then \ - echo " OCAMLC -a $@";\ - $(OCAMLC) $(OCAMLARCHIVEOPTIONS) -a -o $@ \ - $(IMPLEMENTATION_FILES:%.ml=%.cmo); fi - -$(ARCHIVE_OPT): $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(LIBRARIES_OPT) - $(H)if [ $(PACKAGE) != dummy ]; then \ - echo " OCAMLOPT -a $@";\ - $(OCAMLOPT) $(OCAMLARCHIVEOPTIONS) -a -o $@ \ - $(IMPLEMENTATION_FILES:%.ml=%.cmx); fi - -prereq: $(PREREQ) -all: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(ARCHIVE) - @echo -n -opt: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(ARCHIVE_OPT) - @echo -n -test: test.ml $(ARCHIVE) - $(OCAMLC) $(ARCHIVE) -linkpkg -o $@ $< -test.opt: test.ml $(ARCHIVE_OPT) - $(OCAMLOPT) $(ARCHIVE_OPT) -linkpkg -o $@ $< -install: -uninstall: - -depend:: $(DEPEND_FILES) - $(H)echo " OCAMLDEP" - $(H)$(OCAMLDEP) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend -depend.opt:: $(DEPEND_FILES) - $(H)echo " OCAMLDEP -native" - $(H)$(OCAMLDEP) -native \ - $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend.opt - -$(PACKAGE).ps: .dep.dot - dot -Tps -o $@ $< - -# FG: .depend or .depend.opt? -.dep.dot: .depend - ocamldot < .depend > $@ - -%.cmi: %.mli - @echo " OCAMLC $<" - $(H)$(OCAMLC) -c $< -%.cmo %.cmi: %.ml - @echo " OCAMLC $<" - $(H)$(OCAMLC) -c $< -%.cmx: %.ml - @echo " OCAMLOPT $<" - $(H)$(OCAMLOPT) -c $< -%.annot: %.ml - $(OCAMLC) -dtypes $(PKGS) -c $< -%.ml %.mli: %.mly - $(OCAMLYACC) $< -%.ml: %.mll - $(OCAMLLEX) $< - -ifneq ($(MAKECMDGOALS), clean) -$(IMPLEMENTATION_FILES:%.ml=%.cmo): $(LIBRARIES) -$(IMPLEMENTATION_FILES:%.ml=%.cmi): $(LIBRARIES_DEPS) -$(IMPLEMENTATION_FILES:%.ml=%.cmx): $(LIBRARIES_OPT) -endif - -clean: - rm -f *.cm[ioax] *.cmxa *.o *.a *.annot $(EXTRA_OBJECTS_TO_CLEAN) - if [ -f test ]; then rm -f test; else true; fi - if [ -f test.opt ]; then rm -f test.opt; else true; fi - -backup: - cd ..; tar cvzf $(PACKAGE)_$(shell date +%s).tar.gz $(PACKAGE) - -ocamlinit: - echo "#use \"topfind\";;" > .ocamlinit - echo "#thread;;" >> .ocamlinit - for p in $(REQUIRES); do echo "#require \"$$p\";;" >> .ocamlinit; done - echo "#load \"$(PACKAGE).cma\";;" >> .ocamlinit - -# $(STATS_EXCLUDE) may be defined in libraries' Makefile to exclude some file -# from statistics collection -STATS_FILES = \ - $(shell find . -maxdepth 1 -type f -name \*.ml $(foreach f,$(STATS_EXCLUDE),-not -name $(f))) \ - $(shell find . -maxdepth 1 -type f -name \*.mli $(foreach f,$(STATS_EXCLUDE),-not -name $(f))) -.stats: $(STATS_FILES) - rm -f .stats - echo -n "LOC:" >> .stats - wc -l $(STATS_FILES) | tail -1 | awk '{ print $$1 }' >> .stats - -.PHONY: all opt backup depend depend.opt install uninstall clean ocamlinit - -ifeq ($(MAKECMDGOALS),) - include .depend -endif - -ifeq ($(MAKECMDGOALS), all) - include .depend -endif - -ifeq ($(MAKECMDGOALS), opt) - include .depend.opt -endif - -NULL = diff --git a/matita/configure.ac b/matita/configure.ac deleted file mode 100644 index cf8a8e4ee..000000000 --- a/matita/configure.ac +++ /dev/null @@ -1,218 +0,0 @@ -AC_INIT -AC_CONFIG_SRCDIR([matita/matitaTypes.ml]) - -# Distribution settings -# (i.e. settings (automatically) manipulated before a release) -DEBUG_DEFAULT="true" -DEFAULT_DBHOST="mysql://mowgli.cs.unibo.it" -RT_BASE_DIR_DEFAULT="`pwd`/matita" -MATITA_VERSION="0.99.5" -DISTRIBUTED="yes" # "yes" for distributed tarballs -# End of distribution settings - -SRCROOT=`pwd` -AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no) -if test $HAVE_OCAMLC = "no"; then - AC_MSG_ERROR(could not find ocamlc) -fi -AC_CHECK_PROG(HAVE_OCAMLOPT, ocamlopt, yes, no) -if test $HAVE_OCAMLOPT = "no"; then - AC_MSG_WARN(could not find ocamlopt: native code compilation disabled) -fi -AC_CHECK_PROG(HAVE_OCAMLFIND, ocamlfind, yes, no) -if test $HAVE_OCAMLFIND = "yes"; then - OCAMLFIND="ocamlfind" -else - AC_MSG_ERROR(could not find ocamlfind) -fi -AC_CHECK_PROG(HAVE_LABLGLADECC, lablgladecc3, yes, no) -if test $HAVE_LABLGLADECC = "yes"; then - LABLGLADECC="lablgladecc3" -else - AC_MSG_ERROR(could not find lablgladecc3) -fi -AC_CHECK_PROG(HAVE_CAMLP5O, camlp5o, yes, no) -if test $HAVE_CAMLP5O = "yes"; then - CAMLP5O="camlp5o" -else - AC_MSG_ERROR(could not find camlp5o) -fi - -# look for METAS dir - -LIBSPATH="`pwd`/components" -OCAMLPATHL="$LIBSPATH/METAS" -OCAMLPATH="$OCAMLPATHL:$OCAMLPATH" - -# creating META.* - -echo -n "creating METAs ... " -for f in $OCAMLPATHL/meta.*.src; do - basename=`basename $f` - metaname=`echo $basename | sed 's/meta\.\(.*\)\.src/\1/'` - dirname=`echo $metaname | sed 's/^helm-//'` - metafile="$OCAMLPATHL/META.$metaname" - cp $f $metafile - echo "directory=\"$LIBSPATH/$dirname\"" >> $metafile -done -echo "done" - -# (libs) findlib requisites - -#gdome2 \ -#mysql \ -FINDLIB_LIBSREQUIRES="\ -expat \ -http \ -camlp-streams \ -pcre \ -str \ -unix \ -lablgtk3 \ -lablgtk3-sourceview3 \ -netstring \ -ulex-camlp5 \ -zip \ -" - -# (Matita) findlib requisites - -#lablgtk3.glade \ -FINDLIB_COMREQUIRES="\ -helm-disambiguation \ -helm-grafite \ -helm-grafite_engine \ -helm-ng_disambiguation \ -helm-ng_cic_content \ -helm-grafite_parser \ -helm-content_pres \ -helm-ng_paramodulation \ -helm-ng_tactics \ -" -FINDLIB_CREQUIRES=" \ -$FINDLIB_COMREQUIRES \ -" -FINDLIB_REQUIRES="\ -$FINDLIB_CREQUIRES \ -lablgtk3-sourceview3 \ -" - -for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES -do - AC_MSG_CHECKING(for $r ocaml library) - if OCAMLPATH=$OCAMLPATH $OCAMLFIND query $r &> /dev/null; then - AC_MSG_RESULT(yes) - else - AC_MSG_ERROR(could not find $r ocaml library) - fi -done - -OCAMLFIND_COMMANDS="" -# AC_CHECK_PROG(HAVE_OCAMLC_OPT, ocamlc.opt, yes, no) -# if test $HAVE_OCAMLC_OPT = "yes"; then -# if test "$OCAMLFIND_COMMANDS" = ""; then -# OCAMLFIND_COMMANDS="ocamlc=ocamlc.opt" -# else -# OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlc=ocamlc.opt" -# fi -# fi -# AC_CHECK_PROG(HAVE_OCAMLOPT_OPT, ocamlopt.opt, yes, no) -# if test $HAVE_OCAMLOPT_OPT = "yes"; then -# if test "$OCAMLFIND_COMMANDS" = ""; then -# OCAMLFIND_COMMANDS="ocamlopt=ocamlopt.opt" -# else -# OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlopt=ocamlopt.opt" -# fi -# fi -if test "$OCAMLFIND_COMMANDS" != ""; then - OCAMLFIND="OCAMLFIND_COMMANDS='$OCAMLFIND_COMMANDS' $OCAMLFIND" -fi - -AC_MSG_CHECKING(--enable-debug argument) -AC_ARG_ENABLE(debug, - [ --enable-debug Turn on debugging], - [GIVEN="yes"; - case "${enableval}" in - yes) DEBUG=true ;; - no) DEBUG=false ;; - *) AC_MSG_ERROR(bad value ${enableval} for --enable-debug) ;; - esac], - [GIVEN="no"; DEBUG="$DEBUG_DEFAULT"]) -MSG=$GIVEN -if test "$DEBUG" = "true"; then - MSG="$MSG, debugging enabled." -else - MSG="$MSG, debugging disabled." -fi -AC_MSG_RESULT($MSG) - -AC_MSG_CHECKING(--enable-annot argument) -AC_ARG_ENABLE(annot, - [ --enable-annot Turn on -dtypes compilation option], - [GIVEN="yes"; - case "${enableval}" in - yes) ANNOT=true;; - no) ANNOT=false;; - *) AC_MSG_ERROR(bad value ${enableval} for --enable-annot) ;; - esac], - [GIVEN="no"; ANNOT="false"]) -MSG=$GIVEN -if test "$ANNOT" = "true"; then - MSG="$MSG, type annotation enabled." -else - MSG="$MSG, type annotation disabled." -fi -AC_MSG_RESULT($MSG) - - -AC_MSG_CHECKING(--with-runtime-dir argument) -AC_ARG_WITH(runtime-dir, - [ --with-runtime-dir Runtime directory (current working directory if not given)], - [ RT_BASE_DIR="${withval}" ], - [ RT_BASE_DIR="$RT_BASE_DIR_DEFAULT" ]) -MSG="$RT_BASE_DIR" -if test "yes" = "$RT_BASE_DIR"; then - MSG=" -** error: ** -** empty --with-runtime-dir argument, please use --with-runtime-dir=value **" -fi -AC_MSG_RESULT($MSG) - -AC_MSG_CHECKING(--with-dbhost argument) -AC_ARG_WITH(dbhost, - [ --with-dbhost SQL database hostname], - [ DBHOST="${withval}" ], - [ DBHOST="$DEFAULT_DBHOST" ]) -MSG="$DBHOST" -if test "yes" = "$DBHOST"; then - MSG=" -** error: ** -** empty --with-dbhost argument, please use --with-dbhost=value **" -fi -AC_MSG_RESULT($MSG) - -AC_SUBST(CAMLP5O) -AC_SUBST(DBHOST) -AC_SUBST(DEBUG) -AC_SUBST(ANNOT) -AC_SUBST(DISTRIBUTED) -AC_SUBST(FINDLIB_CREQUIRES) -AC_SUBST(FINDLIB_REQUIRES) -AC_SUBST(HAVE_OCAMLOPT) -AC_SUBST(LABLGLADECC) -AC_SUBST(MATITA_VERSION) -AC_SUBST(OCAMLFIND) -AC_SUBST(OCAMLPATH) -AC_SUBST(RT_BASE_DIR) -AC_SUBST(SRCROOT) -AC_SUBST(TRANSFORMER_MODULE) - -AC_CONFIG_FILES([ - components/extlib/componentsConf.ml - matita/matita.conf.xml - matita/buildTimeConf.ml - matita/help/C/version.txt - Makefile.defs -]) -AC_OUTPUT - diff --git a/matita/matita.install b/matita/matita.install index d8d93e4e8..b1007b300 100644 --- a/matita/matita.install +++ b/matita/matita.install @@ -13,6 +13,17 @@ share_root: [ "_build/install/default/share/matita/myshare/LICENSE" {"matita/myshare/LICENSE"} "_build/install/default/share/matita/myshare/closed.xml" {"matita/myshare/closed.xml"} "_build/install/default/share/matita/myshare/help/C/declarative_tactics_quickref.xml" {"matita/myshare/help/C/declarative_tactics_quickref.xml"} + "_build/install/default/share/matita/myshare/help/C/figures/database.dia" {"matita/myshare/help/C/figures/database.dia"} + "_build/install/default/share/matita/myshare/help/C/figures/database.png" {"matita/myshare/help/C/figures/database.png"} + "_build/install/default/share/matita/myshare/help/C/figures/matita.png" {"matita/myshare/help/C/figures/matita.png"} + "_build/install/default/share/matita/myshare/help/C/figures/vbox1.png" {"matita/myshare/help/C/figures/vbox1.png"} + "_build/install/default/share/matita/myshare/help/C/figures/vbox2.png" {"matita/myshare/help/C/figures/vbox2.png"} + "_build/install/default/share/matita/myshare/help/C/figures/vbox3.png" {"matita/myshare/help/C/figures/vbox3.png"} + "_build/install/default/share/matita/myshare/help/C/figures/vbox35.png" {"matita/myshare/help/C/figures/vbox35.png"} + "_build/install/default/share/matita/myshare/help/C/figures/vbox4.png" {"matita/myshare/help/C/figures/vbox4.png"} + "_build/install/default/share/matita/myshare/help/C/figures/vbox5.png" {"matita/myshare/help/C/figures/vbox5.png"} + "_build/install/default/share/matita/myshare/help/C/figures/vbox6.png" {"matita/myshare/help/C/figures/vbox6.png"} + "_build/install/default/share/matita/myshare/help/C/figures/vbox7.png" {"matita/myshare/help/C/figures/vbox7.png"} "_build/install/default/share/matita/myshare/help/C/legal.xml" {"matita/myshare/help/C/legal.xml"} "_build/install/default/share/matita/myshare/help/C/matita.xml" {"matita/myshare/help/C/matita.xml"} "_build/install/default/share/matita/myshare/help/C/sec_commands.xml" {"matita/myshare/help/C/sec_commands.xml"} @@ -374,6 +385,17 @@ doc: [ "_build/install/default/doc/matita/html/command_unification_hint.html" {"html/command_unification_hint.html"} "_build/install/default/doc/matita/html/command_universe_constraints.html" {"html/command_universe_constraints.html"} "_build/install/default/doc/matita/html/docbook.css" {"html/docbook.css"} + "_build/install/default/doc/matita/html/figures/database.dia" {"html/figures/database.dia"} + "_build/install/default/doc/matita/html/figures/database.png" {"html/figures/database.png"} + "_build/install/default/doc/matita/html/figures/matita.png" {"html/figures/matita.png"} + "_build/install/default/doc/matita/html/figures/vbox1.png" {"html/figures/vbox1.png"} + "_build/install/default/doc/matita/html/figures/vbox2.png" {"html/figures/vbox2.png"} + "_build/install/default/doc/matita/html/figures/vbox3.png" {"html/figures/vbox3.png"} + "_build/install/default/doc/matita/html/figures/vbox35.png" {"html/figures/vbox35.png"} + "_build/install/default/doc/matita/html/figures/vbox4.png" {"html/figures/vbox4.png"} + "_build/install/default/doc/matita/html/figures/vbox5.png" {"html/figures/vbox5.png"} + "_build/install/default/doc/matita/html/figures/vbox6.png" {"html/figures/vbox6.png"} + "_build/install/default/doc/matita/html/figures/vbox7.png" {"html/figures/vbox7.png"} "_build/install/default/doc/matita/html/index.html" {"html/index.html"} "_build/install/default/doc/matita/html/inst_from_src.html" {"html/inst_from_src.html"} "_build/install/default/doc/matita/html/macro_intro.html" {"html/macro_intro.html"} diff --git a/matita/matita/Makefile b/matita/matita/Makefile deleted file mode 100644 index c0a7903dc..000000000 --- a/matita/matita/Makefile +++ /dev/null @@ -1,400 +0,0 @@ -export SHELL=/bin/bash - -include ../Makefile.defs - -NULL = -H=@ - -ifeq ($(ANNOT),true) - ANNOTOPTION = -dtypes -else - ANNOTOPTION = -endif - -#OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-70-31 -OCAML_FLAGS = -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-70-31-29 -OCAMLDEP_FLAGS = -pp $(CAMLP5O) -PKGS = -package "$(MATITA_REQUIRES)" -CPKGS = -package "$(MATITA_CREQUIRES)" -OCAML_THREADS_FLAGS = -thread -OCAML_DEBUG_FLAGS = -g -#OCAML_PROF=p -p a -#OCAMLOPT_DEBUG_FLAGS = -p -OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) -OCAMLC = $(OCAMLFIND) ocamlc$(OCAML_PROF) $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) -OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) $(OCAMLOPT_DEBUG_FLAGS) -OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAMLDEP_FLAGS) -INSTALL_PROGRAMS= matita matitac matitaclean -INSTALL_PROGRAMS_LINKS_MATITA= -INSTALL_PROGRAMS_LINKS_MATITAC= - -MATITA_FLAGS = -noprofile -NODB=false -ifeq ($(NODB),true) - MATITA_FLAGS += -nodb -endif - -MLI = \ - lablGraphviz.mli \ - matitaTypes.mli \ - matitaMiscCli.mli \ - matitaMisc.mli \ - applyTransformation.mli \ - matitaEngine.mli \ - matitaExcPp.mli \ - matitaInit.mli \ - matitaGtkMisc.mli \ - virtuals.mli \ - cicMathView.mli \ - predefined_virtuals.mli \ - matitaMathView.mli \ - matitaScript.mli \ - matitaGui.mli \ - $(NULL) -CMLI = \ - matitaTypes.mli \ - matitaMiscCli.mli \ - applyTransformation.mli \ - matitaEngine.mli \ - matitaExcPp.mli \ - matitaInit.mli \ - $(NULL) -MAINCMLI = \ - $(NULL) -# objects for matita (GTK GUI) -ML = buildTimeConf.ml matitaGuiInit.ml matitaGeneratedGui.ml $(MLI:%.mli=%.ml) -# objects for matitac (batch compiler) -CML = buildTimeConf.ml $(CMLI:%.mli=%.ml) -MAINCML = $(MAINCMLI:%.mli=%.ml) - -PROGRAMS_BYTE = \ - matita matitac matitaclean -PROGRAMS = $(PROGRAMS_BYTE) -PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) -NOINST_PROGRAMS = -NOINST_PROGRAMS_OPT = $(patsubst %,%.opt,$(EXTRA_PROGRAMS)) - -.PHONY: all -all: $(PROGRAMS) $(NOINST_PROGRAMS) - -CMOS = $(ML:%.ml=%.cmo) -CCMOS = $(CML:%.ml=%.cmo) -MAINCMOS = $(MAINCML:%.ml=%.cmo) -CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) -CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) -MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS)) -$(CMOS) : $(LIB_DEPS) -$(CMXOS): $(LIBX_DEPS) - -LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_REQUIRES)) -LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES)) -CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_CREQUIRES)) -CLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_CREQUIRES)) -opt: $(PROGRAMS_OPT) $(NOINST_PROGRAMS_OPT) -upx: $(PROGRAMS_UPX) -.PHONY: opt upx - -ifeq ($(HAVE_OCAMLOPT),yes) -world: depend.opt opt links -else -world: depend all -endif - -#links %.opt -> % -links: - $(H)for X in $(INSTALL_PROGRAMS_LINKS_MATITAC) \ - $(INSTALL_PROGRAMS_LINKS_MATITA); do\ - ln -sf $$X.opt $$X;\ - done - $(H)ln -sf matita.opt matita - $(H)ln -sf matitac.opt matitac - $(H)ln -sf matitaclean.opt matitaclean - -linkonly: - $(H)echo " OCAMLC matita.ml" - $(H)$(OCAMLC) $(PKGS) -linkpkg -o matita $(CMOS) $(OCAML_DEBUG_FLAGS) matita.ml - $(H)echo " OCAMLC matitac.ml" - $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitac.ml - $(H)echo " OCAMLC matitaclean.ml" - $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitaclean $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitaclean.ml -.PHONY: linkonly -matita: matita.ml $(LIB_DEPS) $(CMOS) - $(H)echo " OCAMLC $<" - $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml -matita.opt: matita.ml $(LIBX_DEPS) $(CMXS) - $(H)echo " OCAMLOPT $<" - $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml - -matitac: matitac.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) - $(H)echo " OCAMLC $<" - $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml -matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) - $(H)echo " OCAMLOPT $<" - $(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml - -matitaclean: matitaclean.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) - $(H)echo " OCAMLC $<" - $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitaclean.ml -matitaclean.opt: matitaclean.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) - $(H)echo " OCAMLOPT $<" - $(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitaclean.ml - -rottener: rottener.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) - $(H)echo " OCAMLC $<" - $(H)$(OCAMLC) $(CPKGS) -package lablgtk2 -linkpkg -o $@ $(CCMOS) $(MAINCMOS) rottener.ml -rottener.opt: rottener.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) - $(H)echo " OCAMLOPT $<" - $(H)$(OCAMLOPT) $(CPKGS) -package lablgtk2 -linkpkg -o $@ $(CCMXS) $(MAINCMXS) rottener.ml -clean-rottened: - find . -type f -name "*.ma.*.rottened" -exec rm {} \; - -matitaGeneratedGui.ml: matita.ui - $(H)$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml - - -.PHONY: clean -clean: - $(H)rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ - $(PROGRAMS) $(PROGRAMS_OPT) \ - rottener rottener.opt \ - $(NOINST_PROGRAMS) $(NOINST_PROGRAMS_OPT) \ - $(PROGRAMS_STATIC) \ - $(PROGRAMS_UPX) \ - *.stamp \ - $(NULL) - -.PHONY: distclean -distclean: clean - $(H)$(MAKE) -C dist/ clean - $(H)rm -f buildTimeConf.ml - $(H)rm -f matita.glade.bak matita.gladep.bak - $(H)rm -f matita.conf.xml.sample - $(H)rm -rf .matita - -TEST_DIRS = \ - legacy \ - library \ - contribs/character \ - tests \ - contribs/dama/dama \ - contribs/assembly \ - contribs/CoRN \ - contribs/RELATIONAL \ - contribs/LOGIC \ - contribs/limits \ - $(NULL) - -# library_auto -TEST_DIRS_OPT = \ - $(TEST_DIRS) \ -# contribs/LAMBDA-TYPES \ - $(NULL) - -.PHONY: tests tests.opt cleantests cleantests.opt -tests: $(foreach d,$(TEST_DIRS),$(d)-test) -tests.opt: $(foreach d,$(TEST_DIRS_OPT),$(d)-test-opt) -cleantests: $(foreach d,$(TEST_DIRS),$(d)-cleantests) -cleantests.opt: $(foreach d,$(TEST_DIRS_OPT),$(d)-cleantests-opt) - -%-test: matitac matitaclean - -cd $* && make -k clean all -%-test-opt: matitac.opt matitaclean.opt - -cd $* && make -k clean.opt opt -%-cleantests: matitaclean - -cd $* && make clean -%-cleantests-opt: matitaclean.opt - -cd $* && make clean.opt - -# {{{ Distribution stuff - -dist_pre: - $(MAKE) -C dist/ dist_pre - -WHERE = $(DESTDIR)/$(RT_BASE_DIR) -INSTALL_STUFF = \ - icons/ \ - help/ \ - matita.gtkrc \ - matita.lang \ - matita.ma.templ \ - matita.conf.xml \ - closed.xml \ - AUTHORS \ - LICENSE \ - $(NULL) - -ifeq ($(HAVE_OCAMLOPT),yes) -INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS:%=%.opt) -else -INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS) -endif - -install-arch: install_preliminaries -install-indep: - -install_preliminaries : install_preliminaries.stamp - -install_preliminaries.stamp: - $(H)install -d $(WHERE)/ma/ - $(H)cp -a $(INSTALL_STUFF) $(WHERE) -ifeq ($(HAVE_OCAMLOPT),yes) - $(H)install -s $(INSTALL_STUFF_BIN) $(WHERE) - $(H)for p in $(INSTALL_PROGRAMS); do ln -fs $$p.opt $(WHERE)/$$p; done -else - $(H)install $(INSTALL_STUFF_BIN) $(WHERE) -endif - $(H)for p in $(INSTALL_PROGRAMS_LINKS_MATITAC); do \ - ln -fs matitac $(WHERE)/$$p;\ - done - $(H)for p in $(INSTALL_PROGRAMS_LINKS_MATITA); do \ - ln -fs matita $(WHERE)/$$p;\ - done - $(H)cp -a lib $(WHERE)/lib - - $(H)touch install_preliminaries.stamp - -uninstall: - $(H)rm -rf $(WHERE) - -STATIC_LINK = dist/static_link/static_link -# for matita -STATIC_LIBS = \ - t1 t1x \ - gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \ - gtksourceview-1.0 \ - gdome gmetadom_gdome_cpp_smart \ - stdc++ \ - mysqlclient \ - expat \ - $(NULL) -STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++ -# for matitac & co -STATIC_CLIBS = \ - gdome \ - mysqlclient \ - $(NULL) -STATIC_CLIBS_PROVER = \ - $(STATIC_CLIBS) \ - z \ - pcre \ - expat \ - xml2 \ - glib-2.0 \ - $(NULL) -STATIC_EXTRA_CLIBS = -PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT)) -PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC)) - -ifeq ($(HAVE_OCAMLOPT),yes) -static: $(STATIC_LINK) $(PROGRAMS_STATIC) -else -upx: - $(H)echo "Native code compilation is disabled" -static: - $(H)echo "Native code compilation is disabled" -endif - -$(STATIC_LINK): - $(MAKE) -C dist/ $(STATIC_LINK) - -matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml - $(STATIC_LINK) $(STATIC_LIBS) -- \ - $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \ - $(STATIC_EXTRA_LIBS) - strip $@ -matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml - $(STATIC_LINK) $(STATIC_CLIBS) -- \ - $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \ - $(STATIC_EXTRA_CLIBS) - strip $@ - -%.upx: % - cp $< $@ - strip $@ - upx $@ - -matitaclean.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitaclean.ml - $(STATIC_LINK) $(STATIC_CLIBS) -- \ - $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitaclean.ml \ - $(STATIC_EXTRA_CLIBS) - strip $@ - -%.upx: % - cp $< $@ - strip $@ - upx $@ - -# }}} End of distribution stuff - -# {{{ Deps and automatic rules -tags: TAGS -.PHONY: TAGS -TAGS: - $(H)cd ..; otags -vi -r components/ matita/ - -.PHONY: depend - -depend: - $(H)echo " OCAMLDEP" - $(H)$(OCAMLDEP) *.ml *.mli > .depend -depend.opt: - $(H)echo " OCAMLDEP -native" - $(H)$(OCAMLDEP) -native *.ml *.mli > .depend.opt - -# this should be sligtly better, since should work with 'make all opt' -MAKECMDGOALS_DELIM=$(addprefix _x_,$(addsuffix _x_,$(MAKECMDGOALS))) -ifneq (,$(findstring _x_all_x_,$(MAKECMDGOALS_DELIM))) - # if we 'make all opt' the deps for 'all' should be fine also for opt - # if we 'make opt all' it should not work... - INCLUDE_MANDATORY=yes - TO_INCLUDE+=.depend - TO_DEPEND_ON=$(LIB_DEPS) -else ifneq (,$(findstring _x_opt_x_,$(MAKECMDGOALS_DELIM))) - INCLUDE_MANDATORY=yes - TO_INCLUDE+=.depend.opt - TO_DEPEND_ON=$(LIBX_DEPS) -else ifneq (,$(findstring _x_world_x_,$(MAKECMDGOALS_DELIM))) - ifeq ($(HAVE_OCAMLOPT),yes) - INCLUDE_MANDATORY=yes - TO_INCLUDE+=.depend.opt - TO_DEPEND_ON=$(LIBX_DEPS) - else - INCLUDE_MANDATORY=yes - TO_INCLUDE+=.depend - TO_DEPEND_ON=$(LIB_DEPS) - endif -else - TO_INCLUDE+=.depend - INCLUDE_MANDATORY=no - TO_DEPEND_ON=$(LIB_DEPS) -endif - -$(MLI:%.mli=%.cmi) $(ML:%.ml=%.cmo) $(ML:%.ml=%.cmx): $(TO_DEPEND_ON) - -ifeq (no,$(INCLUDE_MANDATORY)) - -include $(TO_INCLUDE) -else - include $(TO_INCLUDE) -endif - -%.cmi: %.mli - $(H)echo " OCAMLC $<" - $(H)$(OCAMLC) $(PKGS) -c $< -%.cmo %.cmi: %.ml - $(H)echo " OCAMLC $<" - $(H)$(OCAMLC) $(PKGS) -c $< -%.cmx: %.ml - $(H)echo " OCAMLOPT $<" - $(H)$(OCAMLOPT) $(PKGS) -c $< -%.annot: %.ml - $(H)echo " OCAMLC -dtypes $<" - $(H)$(OCAMLC) -dtypes $(PKGS) -c $< - -deps.ps: deps.dot - dot -Tps -o $@ $< -deps.dot: .depend - ./dep2dot.rb < $< | tred > $@ - -# }}} End of deps and automatic rules - -# vim: set foldmethod=marker: diff --git a/matita/matita/dune b/matita/matita/dune index f1798f020..4f0141916 100644 --- a/matita/matita/dune +++ b/matita/matita/dune @@ -9,6 +9,12 @@ (module mysites) (sites matita)) +(rule + (target matitaGeneratedGui.ml) + (deps matita.ui) + (mode (promote)) + (action (with-stdout-to %{target} (run lablgladecc3 -embed %{deps})))) + (executable (name matita) (public_name matita) @@ -29,7 +35,8 @@ (section (site (matita myshare))) (files (glob_files_rec lib/*) - (glob_files_rec help/*) ; brutal + (glob_files_rec help/C/*.xml) + (glob_files_rec help/C/figures/*) (glob_files_rec icons/*) matita.gtkrc matita.lang diff --git a/matita/matita/help/C/matita.pdf b/matita/matita/help/C/matita.pdf index 78a10f2a3..ca6723258 100644 Binary files a/matita/matita/help/C/matita.pdf and b/matita/matita/help/C/matita.pdf differ diff --git a/matita/matita/matitaGeneratedGui.ml b/matita/matita/matitaGeneratedGui.ml new file mode 100644 index 000000000..390f079ca --- /dev/null +++ b/matita/matita/matitaGeneratedGui.ml @@ -0,0 +1,880 @@ +(* Automatically generated from matita.ui by lablgladecc *) + +let data = "\n\n\n \n \n 600\n 400\n True\n False\n Auto\n dialog\n south-east\n \n \n True\n False\n vertical\n \n \n True\n False\n 2\n \n \n True\n True\n in\n \n \n True\n False\n \n \n True\n False\n \n \n \n \n \n \n True\n True\n 0\n \n \n \n \n True\n False\n vertical\n \n \n True\n True\n False\n \n \n True\n False\n 0\n 0\n \n \n True\n False\n 2\n \n \n True\n False\n gtk-go-up\n \n \n False\n False\n 0\n \n \n \n \n True\n False\n True\n \n \n False\n False\n 1\n \n \n \n \n \n \n \n \n True\n True\n 0\n \n \n \n \n True\n True\n False\n \n \n True\n False\n gtk-go-down\n \n \n \n \n True\n True\n 1\n \n \n \n \n False\n False\n 1\n \n \n \n \n True\n True\n 0\n \n \n \n \n True\n False\n \n \n False\n True\n 3\n 1\n \n \n \n \n True\n False\n \n \n True\n False\n Last:\n 0\n \n \n True\n True\n 0\n \n \n \n \n True\n False\n 4\n 4\n end\n \n \n gtk-media-pause\n True\n True\n True\n False\n True\n \n \n False\n False\n 0\n \n \n \n \n gtk-media-play\n True\n True\n True\n False\n True\n \n \n False\n False\n 1\n \n \n \n \n gtk-media-next\n True\n True\n True\n False\n True\n \n \n False\n False\n 2\n \n \n \n \n gtk-close\n True\n True\n True\n False\n True\n \n \n False\n False\n 3\n \n \n \n \n True\n True\n 1\n \n \n \n \n False\n True\n 2\n \n \n \n \n \n \n 500\n 480\n True\n False\n Cic browser\n center-on-parent\n 500\n 480\n True\n \n \n True\n False\n \n \n True\n False\n vertical\n \n \n True\n False\n \n \n True\n False\n _File\n True\n \n \n False\n \n \n True\n False\n _New\n True\n \n \n \n \n True\n False\n Open _Location ...\n True\n \n \n \n \n \n True\n False\n \n \n \n \n True\n False\n _Quit\n True\n \n \n \n \n \n \n \n \n True\n False\n _Edit\n True\n \n \n False\n \n \n True\n False\n _Copy\n True\n \n \n \n \n \n \n \n \n False\n False\n 0\n \n \n \n \n True\n False\n 0\n 0\n none\n \n \n True\n False\n \n \n True\n True\n False\n none\n \n \n True\n False\n gtk-new\n \n \n \n \n False\n False\n 0\n \n \n \n \n True\n True\n False\n none\n \n \n True\n False\n gtk-go-back\n \n \n \n \n False\n False\n 1\n \n \n \n \n True\n True\n False\n none\n \n \n True\n False\n gtk-go-forward\n \n \n \n \n False\n False\n 2\n \n \n \n \n True\n True\n True\n False\n refresh\n none\n \n \n True\n False\n gtk-refresh\n \n \n \n \n False\n False\n 3\n \n \n \n \n True\n True\n True\n False\n home\n none\n \n \n True\n False\n gtk-home\n \n \n \n \n False\n False\n 4\n \n \n \n \n True\n False\n gtk-jump-to\n 2\n \n \n False\n False\n 3\n 5\n \n \n \n \n True\n False\n \n \n True\n True\n True\n \226\151\143\n \n \n True\n True\n 0\n \n \n \n \n True\n True\n 6\n \n \n \n \n \n \n False\n True\n 1\n \n \n \n \n True\n True\n \n \n True\n True\n \n \n \n \n True\n False\n MathView\n \n \n False\n \n \n \n \n True\n True\n in\n \n \n True\n True\n False\n \n \n \n \n \n \n \n 1\n \n \n \n \n True\n False\n WhelpResult\n \n \n 1\n False\n \n \n \n \n True\n True\n \n \n True\n False\n none\n \n \n True\n False\n gtk-missing-image\n \n \n \n \n \n \n 2\n \n \n \n \n True\n False\n WhelpEasterEgg\n \n \n 2\n False\n \n \n \n \n True\n True\n \n \n 3\n \n \n \n \n True\n False\n Graph\n \n \n 3\n False\n \n \n \n \n True\n False\n vertical\n \n \n True\n True\n 3\n in\n \n \n True\n True\n 0\n \n \n \n \n True\n False\n 4\n 4\n \n \n True\n False\n vertical\n \n \n True\n True\n 0\n \n \n \n \n True\n True\n True\n \n \n True\n True\n 1\n \n \n \n \n True\n True\n False\n \n \n True\n False\n 0\n 0\n \n \n True\n False\n 2\n \n \n True\n False\n gtk-find\n \n \n False\n False\n 0\n \n \n \n \n True\n False\n Search\n True\n \n \n False\n False\n 1\n \n \n \n \n \n \n \n \n False\n False\n 2\n \n \n \n \n False\n True\n 1\n \n \n \n \n 4\n \n \n \n \n True\n False\n SearchText\n \n \n 4\n False\n \n \n \n \n True\n True\n 3\n \n \n \n \n \n \n \n \n 450\n 400\n False\n title\n True\n dialog\n \n \n True\n False\n vertical\n \n \n True\n False\n spread\n \n \n False\n False\n end\n 0\n \n \n \n \n True\n False\n vertical\n \n \n True\n False\n some informative message here ...\n \n \n False\n False\n 0\n \n \n \n \n True\n True\n True\n in\n \n \n 717\n True\n True\n False\n \n \n \n \n \n \n \n True\n True\n 1\n \n \n \n \n False\n True\n 2\n \n \n \n \n \n \n False\n 5\n Find & Replace\n False\n mouse\n dialog\n \n \n True\n False\n 9\n \n \n True\n False\n Find:\n 0\n \n \n 0\n 0\n \n \n \n \n True\n False\n Replace with: \n 0\n \n \n 0\n 1\n \n \n \n \n True\n True\n True\n True\n \n \n 1\n 0\n \n \n \n \n True\n True\n \n \n 1\n 1\n \n \n \n \n True\n False\n 5\n True\n \n \n gtk-find\n True\n True\n False\n True\n \n \n False\n False\n 1\n \n \n \n \n True\n True\n False\n \n \n True\n False\n 0\n 0\n \n \n True\n False\n 2\n \n \n True\n False\n gtk-find-and-replace\n \n \n False\n False\n 0\n \n \n \n \n True\n False\n _Replace\n True\n \n \n False\n False\n 1\n \n \n \n \n \n \n \n \n False\n False\n 2\n \n \n \n \n gtk-cancel\n True\n True\n False\n True\n \n \n False\n False\n 3\n \n \n \n \n 0\n 2\n 2\n \n \n \n \n \n \n False\n Matita\n \n \n True\n False\n \n \n True\n False\n vertical\n \n \n True\n False\n \n \n True\n False\n _File\n True\n \n \n False\n \n \n True\n False\n _New\n True\n \n \n \n \n \n True\n False\n _Open...\n True\n \n \n \n \n \n True\n False\n _Save\n True\n \n \n \n \n \n True\n False\n _Save as...\n True\n \n \n \n \n \n True\n False\n \n \n \n \n True\n False\n _Close\n True\n \n \n \n \n \n True\n False\n _Quit\n True\n \n \n \n \n \n \n \n \n \n True\n False\n _Edit\n True\n \n \n False\n \n \n True\n False\n False\n _Undo\n True\n \n \n \n \n \n True\n False\n False\n _Redo\n True\n \n \n \n \n \n True\n False\n \n \n \n \n True\n False\n Cut\n True\n \n \n \n \n \n True\n False\n Copy\n True\n \n \n \n \n \n True\n False\n Paste\n True\n \n \n \n \n \n True\n False\n Paste as pattern\n True\n \n \n \n \n True\n False\n Paste Unicode as TeX\n True\n \n \n \n \n True\n False\n Auto-expand TeX Macros\n True\n True\n \n \n \n \n True\n False\n Delete\n True\n \n \n \n \n True\n False\n \n \n \n \n True\n False\n Select _All\n True\n \n \n \n \n True\n False\n \n \n \n \n True\n False\n Find and replace...\n True\n \n \n \n \n \n True\n False\n \n \n \n \n True\n False\n Next ligature\n True\n \n \n \n \n \n True\n False\n Edit with e_xternal editor\n True\n \n \n \n \n \n \n \n \n True\n False\n _Script\n True\n \n \n False\n \n \n True\n False\n Execute 1 phrase\n True\n \n \n \n \n \n True\n False\n Retract 1 phrase\n True\n \n \n \n \n \n True\n False\n \n \n \n \n True\n False\n Execute all\n True\n \n \n \n \n \n True\n False\n Retract all\n True\n \n \n \n \n \n True\n False\n \n \n \n \n True\n False\n Execute until cursor\n True\n \n \n \n \n \n \n \n \n \n True\n False\n _View\n True\n \n \n False\n \n \n True\n False\n New CIC _browser\n True\n \n \n \n \n \n True\n False\n \n \n \n \n True\n False\n _Fullscreen\n True\n \n \n \n \n \n True\n False\n Natural deduction palette\n True\n \n \n \n \n \n True\n False\n \n \n \n \n True\n False\n Zoom in\n True\n \n \n \n \n \n True\n False\n Zoom out\n True\n \n \n \n \n \n True\n False\n Normal size\n True\n \n \n \n \n \n True\n False\n \n \n \n \n True\n False\n Pretty print notation\n True\n True\n \n \n \n \n True\n False\n Hide coercions\n True\n True\n \n \n \n \n True\n False\n \n \n \n \n True\n False\n Coercions Graph\n True\n \n \n \n \n True\n False\n Hints database\n True\n \n \n \n \n True\n False\n Terms grammar\n True\n \n \n \n \n True\n False\n TeX/UTF-8 table\n True\n \n \n \n \n \n \n \n \n True\n False\n _Debug\n True\n \n \n False\n \n \n True\n False\n \n \n \n \n \n \n \n \n True\n False\n _Help\n True\n \n \n False\n \n \n True\n False\n Contents\n True\n \n \n \n \n \n True\n False\n About\n True\n \n \n \n \n \n \n \n \n False\n False\n 0\n \n \n \n \n True\n False\n \n \n True\n True\n \n \n True\n False\n 2\n \n \n True\n False\n \n \n True\n False\n vertical\n \n \n True\n True\n \n \n True\n False\n vertical\n \n \n True\n True\n True\n \n \n True\n False\n Implication (\226\135\146<sub>i</sub>)\n True\n \n \n \n \n True\n True\n 0\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Conjunction (\226\136\167<sub>i</sub>)\n True\n \n \n \n \n True\n True\n 1\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Disjunction left (\226\136\168<sub>i-l</sub>)\n True\n \n \n \n \n True\n True\n 2\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Disjunction right (\226\136\168<sub>i-r</sub>)\n True\n \n \n \n \n True\n True\n 3\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Negation (\194\172<sub>i</sub>)\n True\n \n \n \n \n True\n True\n 4\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Top (\226\138\164<sub>i</sub>)\n True\n \n \n \n \n True\n True\n 5\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Universal (\226\136\128<sub>i</sub>)\n True\n \n \n \n \n True\n True\n 6\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Existential (\226\136\131<sub>i</sub>)\n True\n \n \n \n \n True\n True\n 7\n \n \n \n \n \n \n True\n False\n Introduction rules\n \n \n \n \n False\n True\n 0\n \n \n \n \n True\n True\n \n \n True\n False\n vertical\n \n \n True\n True\n True\n \n \n True\n False\n Implication (\226\135\146<sub>e</sub>)\n True\n \n \n \n \n True\n True\n 0\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Conjunction left (\226\136\167<sub>e-l</sub>)\n True\n \n \n \n \n True\n True\n 1\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Conjunction right (\226\136\167<sub>e-r</sub>)\n True\n \n \n \n \n True\n True\n 2\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Disjunction (\226\136\168<sub>e</sub>)\n True\n \n \n \n \n True\n True\n 3\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Negation (\194\172<sub>e</sub>)\n True\n \n \n \n \n True\n True\n 4\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Bottom (\226\138\165<sub>e</sub>)\n True\n \n \n \n \n True\n True\n 5\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Universal (\226\136\128<sub>e</sub>)\n True\n \n \n \n \n True\n True\n 6\n \n \n \n \n True\n True\n True\n \n \n True\n False\n Existential (\226\136\131<sub>e</sub>)\n True\n \n \n \n \n True\n True\n 7\n \n \n \n \n \n \n True\n False\n Elimination rules\n \n \n \n \n False\n True\n 1\n \n \n \n \n True\n True\n \n \n True\n False\n vertical\n \n \n Reduction to Absurdity (RAA)\n True\n True\n True\n \n \n True\n True\n 0\n \n \n \n \n Use lemma (lem)\n True\n True\n True\n \n \n True\n True\n 1\n \n \n \n \n Discharge (discharge)\n True\n True\n True\n \n \n True\n True\n 2\n \n \n \n \n \n \n True\n False\n Misc rules\n \n \n \n \n False\n True\n 2\n \n \n \n \n False\n True\n 0\n \n \n \n \n False\n True\n 0\n \n \n \n \n 400\n True\n False\n vertical\n \n \n True\n False\n \n \n True\n False\n both\n \n \n True\n False\n \n \n True\n True\n False\n Retract all\n none\n \n \n True\n False\n gtk-goto-top\n \n \n \n \n \n \n False\n False\n \n \n \n \n True\n False\n \n \n True\n True\n False\n Retract 1 phrase\n none\n \n \n True\n False\n gtk-go-up\n \n \n \n \n \n \n False\n False\n \n \n \n \n True\n False\n \n \n True\n True\n False\n Execute until cursor\n none\n \n \n True\n False\n gtk-jump-to\n \n \n \n \n \n \n False\n False\n \n \n \n \n True\n False\n \n \n True\n True\n False\n Execute 1 phrase\n none\n \n \n True\n False\n gtk-go-down\n \n \n \n \n \n \n False\n False\n \n \n \n \n True\n False\n \n \n True\n True\n False\n Execute all\n none\n \n \n True\n False\n gtk-goto-bottom\n \n \n \n \n \n \n False\n False\n \n \n \n \n True\n True\n 0\n \n \n \n \n True\n False\n vertical\n both\n \n \n True\n False\n \n \n True\n True\n False\n none\n \n \n True\n False\n gtk-stop\n \n \n \n \n \n \n False\n False\n \n \n \n \n False\n True\n 1\n \n \n \n \n False\n False\n 0\n \n \n \n \n True\n True\n True\n \n \n True\n True\n 1\n \n \n \n \n True\n True\n 1\n \n \n \n \n False\n True\n \n \n \n \n 250\n 500\n True\n True\n vertical\n 380\n \n \n True\n True\n True\n \n \n False\n True\n \n \n \n \n True\n False\n \n \n True\n True\n never\n in\n \n \n True\n True\n False\n char\n False\n \n \n \n \n True\n True\n 0\n \n \n \n \n True\n True\n \n \n \n \n True\n True\n \n \n \n \n True\n True\n 0\n \n \n \n \n True\n True\n 1\n \n \n \n \n True\n False\n \n \n True\n False\n \n \n True\n True\n 0\n \n \n \n \n True\n False\n False\n \n \n True\n False\n gtk-missing-image\n \n \n \n \n True\n False\n label14\n \n \n False\n \n \n \n \n True\n False\n gtk-missing-image\n \n \n 1\n \n \n \n \n True\n False\n label15\n \n \n 1\n False\n \n \n \n \n True\n False\n gtk-missing-image\n \n \n 2\n \n \n \n \n True\n False\n label16\n \n \n 2\n False\n \n \n \n \n False\n True\n 1\n \n \n \n \n False\n False\n 2\n \n \n \n \n \n \n \n \n 280\n False\n Uri choice\n True\n center\n dialog\n \n \n True\n False\n vertical\n 4\n \n \n True\n False\n end\n \n \n gtk-cancel\n True\n True\n True\n False\n True\n \n \n False\n False\n 0\n \n \n \n \n True\n True\n True\n False\n \n \n True\n False\n 0\n 0\n \n \n True\n False\n 2\n \n \n True\n False\n gtk-index\n \n \n False\n False\n 0\n \n \n \n \n True\n False\n Try _Selected\n True\n \n \n False\n False\n 1\n \n \n \n \n \n \n \n \n False\n False\n 1\n \n \n \n \n Try Constants\n True\n False\n True\n True\n False\n True\n \n \n False\n False\n 2\n \n \n \n \n gtk-copy\n True\n True\n False\n True\n \n \n False\n False\n 3\n \n \n \n \n True\n True\n True\n False\n \n \n True\n False\n 0\n 0\n \n \n True\n False\n 2\n \n \n True\n False\n gtk-ok\n \n \n False\n False\n 0\n \n \n \n \n True\n False\n bla bla bla\n True\n \n \n False\n False\n 1\n \n \n \n \n \n \n \n \n False\n False\n 4\n \n \n \n \n gtk-go-forward\n True\n True\n True\n False\n True\n \n \n False\n False\n 5\n \n \n \n \n False\n False\n end\n 0\n \n \n \n \n True\n False\n vertical\n 3\n \n \n True\n False\n some informative message here ...\n \n \n False\n False\n 0\n \n \n \n \n 400\n True\n True\n True\n \n \n True\n True\n False\n \n \n \n \n \n \n \n True\n True\n 1\n \n \n \n \n True\n False\n True\n \n \n True\n False\n URI: \n \n \n False\n False\n 0\n \n \n \n \n True\n True\n \n \n True\n True\n 1\n \n \n \n \n True\n True\n 2\n \n \n \n \n False\n True\n 2\n \n \n \n \n \n UriChoiceAbortButton\n \n \n\n" + +class autoWin ?translation_domain () = + let builder = GBuilder.builder ?translation_domain () in + let _ = builder#add_objects_from_string data ["AutoWin"] in + object + val toplevel = + new GWindow.window (GtkWindow.Window.cast (builder#get_object "AutoWin")) + method toplevel = toplevel + val autoWin = + new GWindow.window (GtkWindow.Window.cast (builder#get_object "AutoWin")) + method autoWin = autoWin + val vbox17 = + new GPack.box (GtkPack.Box.cast (builder#get_object "vbox17")) + method vbox17 = vbox17 + val hbox30 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox30")) + method hbox30 = hbox30 + val scrolledwindowAREA = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "scrolledwindowAREA")) + method scrolledwindowAREA = scrolledwindowAREA + val viewportAREA = + new GBin.viewport (GtkBin.Viewport.cast (builder#get_object "viewportAREA")) + method viewportAREA = viewportAREA + val table = + new GPack.grid (GtkPack.Grid.cast (builder#get_object "table")) + method table = table + val vbox18 = + new GPack.box (GtkPack.Box.cast (builder#get_object "vbox18")) + method vbox18 = vbox18 + val buttonUP = + new GButton.button (GtkButton.Button.cast (builder#get_object "buttonUP")) + method buttonUP = buttonUP + val alignment19 = + new GBin.alignment (GtkBin.Alignment.cast (builder#get_object "alignment19")) + method alignment19 = alignment19 + val hbox31 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox31")) + method hbox31 = hbox31 + val image1066 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image1066")) + method image1066 = image1066 + val label30 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label30")) + method label30 = label30 + val buttonDOWN = + new GButton.button (GtkButton.Button.cast (builder#get_object "buttonDOWN")) + method buttonDOWN = buttonDOWN + val image1065 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image1065")) + method image1065 = image1065 + val hseparator3 = + new GObj.widget_full (GtkMisc.Separator.cast (builder#get_object "hseparator3")) + method hseparator3 = hseparator3 + val hbox32 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox32")) + method hbox32 = hbox32 + val labelLAST = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "labelLAST")) + method labelLAST = labelLAST + val hbuttonbox3 = + new GPack.button_box (GtkPack.BBox.cast (builder#get_object "hbuttonbox3")) + method hbuttonbox3 = hbuttonbox3 + val buttonPAUSE = + new GButton.button (GtkButton.Button.cast (builder#get_object "buttonPAUSE")) + method buttonPAUSE = buttonPAUSE + val buttonPLAY = + new GButton.button (GtkButton.Button.cast (builder#get_object "buttonPLAY")) + method buttonPLAY = buttonPLAY + val buttonNEXT = + new GButton.button (GtkButton.Button.cast (builder#get_object "buttonNEXT")) + method buttonNEXT = buttonNEXT + val buttonCLOSE = + new GButton.button (GtkButton.Button.cast (builder#get_object "buttonCLOSE")) + method buttonCLOSE = buttonCLOSE + method reparent parent = + vbox17#misc#reparent parent; + toplevel#destroy () + end +class browserWin ?translation_domain () = + let builder = GBuilder.builder ?translation_domain () in + let _ = builder#add_objects_from_string data ["BrowserWin"] in + object + val toplevel = + new GWindow.window (GtkWindow.Window.cast (builder#get_object "BrowserWin")) + method toplevel = toplevel + val browserWin = + new GWindow.window (GtkWindow.Window.cast (builder#get_object "BrowserWin")) + method browserWin = browserWin + val browserWinEventBox = + new GBin.event_box (GtkBin.EventBox.cast (builder#get_object "BrowserWinEventBox")) + method browserWinEventBox = browserWinEventBox + val browserVBox = + new GPack.box (GtkPack.Box.cast (builder#get_object "BrowserVBox")) + method browserVBox = browserVBox + val menubar2 = + new GMenu.menu_shell (GtkMenu.MenuBar.cast (builder#get_object "menubar2")) + method menubar2 = menubar2 + val browserFileMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "BrowserFileMenu")) + method browserFileMenu = browserFileMenu + val browserFileMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "BrowserFileMenu_menu")) + method browserFileMenu_menu = browserFileMenu_menu + val browserNewMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "BrowserNewMenuItem")) + method browserNewMenuItem = browserNewMenuItem + val browserUrlMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "BrowserUrlMenuItem")) + method browserUrlMenuItem = browserUrlMenuItem + val separatormenuitem1 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separatormenuitem1")) + method separatormenuitem1 = separatormenuitem1 + val browserCloseMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "BrowserCloseMenuItem")) + method browserCloseMenuItem = browserCloseMenuItem + val browserEditMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "BrowserEditMenu")) + method browserEditMenu = browserEditMenu + val browserEditMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "BrowserEditMenu_menu")) + method browserEditMenu_menu = browserEditMenu_menu + val browserCopyMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "BrowserCopyMenuItem")) + method browserCopyMenuItem = browserCopyMenuItem + val frame2 = + new GBin.frame (GtkBin.Frame.cast (builder#get_object "frame2")) + method frame2 = frame2 + val browserHBox = + new GPack.box (GtkPack.Box.cast (builder#get_object "BrowserHBox")) + method browserHBox = browserHBox + val browserNewButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "BrowserNewButton")) + method browserNewButton = browserNewButton + val image303 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image303")) + method image303 = image303 + val browserBackButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "BrowserBackButton")) + method browserBackButton = browserBackButton + val image304 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image304")) + method image304 = image304 + val browserForwardButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "BrowserForwardButton")) + method browserForwardButton = browserForwardButton + val image305 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image305")) + method image305 = image305 + val browserRefreshButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "BrowserRefreshButton")) + method browserRefreshButton = browserRefreshButton + val image229 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image229")) + method image229 = image229 + val browserHomeButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "BrowserHomeButton")) + method browserHomeButton = browserHomeButton + val image190 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image190")) + method image190 = image190 + val image301 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image301")) + method image301 = image301 + val uriHBox = + new GPack.box (GtkPack.Box.cast (builder#get_object "UriHBox")) + method uriHBox = uriHBox + val browserUri = + new GEdit.entry (GtkEdit.Entry.cast (builder#get_object "browserUri")) + method browserUri = browserUri + val mathOrListNotebook = + new GPack.notebook (GtkPack.Notebook.cast (builder#get_object "mathOrListNotebook")) + method mathOrListNotebook = mathOrListNotebook + val scrolledBrowser = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "ScrolledBrowser")) + method scrolledBrowser = scrolledBrowser + val mathLabel = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "mathLabel")) + method mathLabel = mathLabel + val scrolledwindow9 = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "scrolledwindow9")) + method scrolledwindow9 = scrolledwindow9 + val whelpResultTreeview = + new GTree.view (GtkTree.TreeView.cast (builder#get_object "whelpResultTreeview")) + method whelpResultTreeview = whelpResultTreeview + val whelpResult = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "WhelpResult")) + method whelpResult = whelpResult + val scrolledwindow11 = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "scrolledwindow11")) + method scrolledwindow11 = scrolledwindow11 + val viewport2 = + new GBin.viewport (GtkBin.Viewport.cast (builder#get_object "viewport2")) + method viewport2 = viewport2 + val browserImage = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "BrowserImage")) + method browserImage = browserImage + val easterEggLabel = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "EasterEggLabel")) + method easterEggLabel = easterEggLabel + val graphScrolledWin = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "GraphScrolledWin")) + method graphScrolledWin = graphScrolledWin + val label26 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label26")) + method label26 = label26 + val vbox20 = + new GPack.box (GtkPack.Box.cast (builder#get_object "vbox20")) + method vbox20 = vbox20 + val scrolledwinContent = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "scrolledwinContent")) + method scrolledwinContent = scrolledwinContent + val hbox35 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox35")) + method hbox35 = hbox35 + val vbox22 = + new GPack.box (GtkPack.Box.cast (builder#get_object "vbox22")) + method vbox22 = vbox22 + val entrySearch = + new GEdit.entry (GtkEdit.Entry.cast (builder#get_object "entrySearch")) + method entrySearch = entrySearch + val buttonSearch = + new GButton.button (GtkButton.Button.cast (builder#get_object "buttonSearch")) + method buttonSearch = buttonSearch + val alignment21 = + new GBin.alignment (GtkBin.Alignment.cast (builder#get_object "alignment21")) + method alignment21 = alignment21 + val hbox36 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox36")) + method hbox36 = hbox36 + val image1068 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image1068")) + method image1068 = image1068 + val label32 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label32")) + method label32 = label32 + val searchText = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "SearchText")) + method searchText = searchText + method reparent parent = + browserWinEventBox#misc#reparent parent; + toplevel#destroy () + end +class disambiguationErrors ?translation_domain () = + let builder = GBuilder.builder ?translation_domain () in + let _ = builder#add_objects_from_string data ["DisambiguationErrors"] in + object + val toplevel = + new GWindow.dialog_any (GtkWindow.Dialog.cast (builder#get_object "DisambiguationErrors")) + method toplevel = toplevel + val disambiguationErrors = + new GWindow.dialog_any (GtkWindow.Dialog.cast (builder#get_object "DisambiguationErrors")) + method disambiguationErrors = disambiguationErrors + val vbox14 = + new GPack.box (GtkPack.Box.cast (builder#get_object "vbox14")) + method vbox14 = vbox14 + val hbuttonbox2 = + new GPack.button_box (GtkPack.BBox.cast (builder#get_object "hbuttonbox2")) + method hbuttonbox2 = hbuttonbox2 + val vbox15 = + new GPack.box (GtkPack.Box.cast (builder#get_object "vbox15")) + method vbox15 = vbox15 + val disambiguationErrorsLabel = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "disambiguationErrorsLabel")) + method disambiguationErrorsLabel = disambiguationErrorsLabel + val scrolledwindow12 = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "scrolledwindow12")) + method scrolledwindow12 = scrolledwindow12 + val treeview = + new GTree.view (GtkTree.TreeView.cast (builder#get_object "treeview")) + method treeview = treeview + method reparent parent = + vbox14#misc#reparent parent; + toplevel#destroy () + end +class findReplWin ?translation_domain () = + let builder = GBuilder.builder ?translation_domain () in + let _ = builder#add_objects_from_string data ["FindReplWin"] in + object + val toplevel = + new GWindow.window (GtkWindow.Window.cast (builder#get_object "FindReplWin")) + method toplevel = toplevel + val findReplWin = + new GWindow.window (GtkWindow.Window.cast (builder#get_object "FindReplWin")) + method findReplWin = findReplWin + val table1 = + new GPack.grid (GtkPack.Grid.cast (builder#get_object "table1")) + method table1 = table1 + val label17 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label17")) + method label17 = label17 + val label18 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label18")) + method label18 = label18 + val findEntry = + new GEdit.entry (GtkEdit.Entry.cast (builder#get_object "findEntry")) + method findEntry = findEntry + val replaceEntry = + new GEdit.entry (GtkEdit.Entry.cast (builder#get_object "replaceEntry")) + method replaceEntry = replaceEntry + val hbox19 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox19")) + method hbox19 = hbox19 + val findButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "findButton")) + method findButton = findButton + val findReplButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "findReplButton")) + method findReplButton = findReplButton + val alignment13 = + new GBin.alignment (GtkBin.Alignment.cast (builder#get_object "alignment13")) + method alignment13 = alignment13 + val hbox20 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox20")) + method hbox20 = hbox20 + val image357 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image357")) + method image357 = image357 + val label19 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label19")) + method label19 = label19 + val cancelButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "cancelButton")) + method cancelButton = cancelButton + method reparent parent = + table1#misc#reparent parent; + toplevel#destroy () + end +class mainWin ?translation_domain () = + let builder = GBuilder.builder ?translation_domain () in + let _ = builder#add_objects_from_string data ["MainWin"] in + object + val toplevel = + new GWindow.window (GtkWindow.Window.cast (builder#get_object "MainWin")) + method toplevel = toplevel + val mainWin = + new GWindow.window (GtkWindow.Window.cast (builder#get_object "MainWin")) + method mainWin = mainWin + val mainWinEventBox = + new GBin.event_box (GtkBin.EventBox.cast (builder#get_object "MainWinEventBox")) + method mainWinEventBox = mainWinEventBox + val vbox8 = + new GPack.box (GtkPack.Box.cast (builder#get_object "vbox8")) + method vbox8 = vbox8 + val menubar1 = + new GMenu.menu_shell (GtkMenu.MenuBar.cast (builder#get_object "menubar1")) + method menubar1 = menubar1 + val fileMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "fileMenu")) + method fileMenu = fileMenu + val fileMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "fileMenu_menu")) + method fileMenu_menu = fileMenu_menu + val newMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "newMenuItem")) + method newMenuItem = newMenuItem + val openMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "openMenuItem")) + method openMenuItem = openMenuItem + val saveMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "saveMenuItem")) + method saveMenuItem = saveMenuItem + val saveAsMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "saveAsMenuItem")) + method saveAsMenuItem = saveAsMenuItem + val separator2 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator2")) + method separator2 = separator2 + val closeMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "closeMenuItem")) + method closeMenuItem = closeMenuItem + val quitMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "quitMenuItem")) + method quitMenuItem = quitMenuItem + val editMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "editMenu")) + method editMenu = editMenu + val editMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "editMenu_menu")) + method editMenu_menu = editMenu_menu + val undoMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "undoMenuItem")) + method undoMenuItem = undoMenuItem + val redoMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "redoMenuItem")) + method redoMenuItem = redoMenuItem + val separator3 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator3")) + method separator3 = separator3 + val cutMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "cutMenuItem")) + method cutMenuItem = cutMenuItem + val copyMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "copyMenuItem")) + method copyMenuItem = copyMenuItem + val pasteMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "pasteMenuItem")) + method pasteMenuItem = pasteMenuItem + val pastePatternMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "pastePatternMenuItem")) + method pastePatternMenuItem = pastePatternMenuItem + val unicodeAsTexMenuItem = + new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (builder#get_object "unicodeAsTexMenuItem")) + method unicodeAsTexMenuItem = unicodeAsTexMenuItem + val menuitemAutoAltL = + new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (builder#get_object "menuitemAutoAltL")) + method menuitemAutoAltL = menuitemAutoAltL + val deleteMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "deleteMenuItem")) + method deleteMenuItem = deleteMenuItem + val separator4 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator4")) + method separator4 = separator4 + val selectAllMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "selectAllMenuItem")) + method selectAllMenuItem = selectAllMenuItem + val separator7 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator7")) + method separator7 = separator7 + val findReplMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "findReplMenuItem")) + method findReplMenuItem = findReplMenuItem + val separator8 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator8")) + method separator8 = separator8 + val ligatureButton = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "LigatureButton")) + method ligatureButton = ligatureButton + val externalEditorMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "externalEditorMenuItem")) + method externalEditorMenuItem = externalEditorMenuItem + val scriptMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "scriptMenu")) + method scriptMenu = scriptMenu + val scriptMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "scriptMenu_menu")) + method scriptMenu_menu = scriptMenu_menu + val scriptAdvanceMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "scriptAdvanceMenuItem")) + method scriptAdvanceMenuItem = scriptAdvanceMenuItem + val scriptRetractMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "scriptRetractMenuItem")) + method scriptRetractMenuItem = scriptRetractMenuItem + val separator9 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator9")) + method separator9 = separator9 + val scriptBottomMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "scriptBottomMenuItem")) + method scriptBottomMenuItem = scriptBottomMenuItem + val scriptTopMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "scriptTopMenuItem")) + method scriptTopMenuItem = scriptTopMenuItem + val separator10 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator10")) + method separator10 = separator10 + val scriptJumpMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "scriptJumpMenuItem")) + method scriptJumpMenuItem = scriptJumpMenuItem + val viewMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "viewMenu")) + method viewMenu = viewMenu + val viewMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "viewMenu_menu")) + method viewMenu_menu = viewMenu_menu + val newCicBrowserMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "newCicBrowserMenuItem")) + method newCicBrowserMenuItem = newCicBrowserMenuItem + val separator5 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator5")) + method separator5 = separator5 + val fullscreenMenuItem = + new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (builder#get_object "fullscreenMenuItem")) + method fullscreenMenuItem = fullscreenMenuItem + val menuitemPalette = + new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (builder#get_object "menuitemPalette")) + method menuitemPalette = menuitemPalette + val separator1 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator1")) + method separator1 = separator1 + val increaseFontSizeMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "increaseFontSizeMenuItem")) + method increaseFontSizeMenuItem = increaseFontSizeMenuItem + val decreaseFontSizeMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "decreaseFontSizeMenuItem")) + method decreaseFontSizeMenuItem = decreaseFontSizeMenuItem + val normalFontSizeMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "normalFontSizeMenuItem")) + method normalFontSizeMenuItem = normalFontSizeMenuItem + val separator12 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator12")) + method separator12 = separator12 + val ppNotationMenuItem = + new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (builder#get_object "ppNotationMenuItem")) + method ppNotationMenuItem = ppNotationMenuItem + val hideCoercionsMenuItem = + new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (builder#get_object "hideCoercionsMenuItem")) + method hideCoercionsMenuItem = hideCoercionsMenuItem + val separator13 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator13")) + method separator13 = separator13 + val showCoercionsGraphMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "showCoercionsGraphMenuItem")) + method showCoercionsGraphMenuItem = showCoercionsGraphMenuItem + val showHintsDbMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "showHintsDbMenuItem")) + method showHintsDbMenuItem = showHintsDbMenuItem + val showTermGrammarMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "showTermGrammarMenuItem")) + method showTermGrammarMenuItem = showTermGrammarMenuItem + val showUnicodeTable = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "showUnicodeTable")) + method showUnicodeTable = showUnicodeTable + val debugMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "debugMenu")) + method debugMenu = debugMenu + val debugMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "debugMenu_menu")) + method debugMenu_menu = debugMenu_menu + val separator6 = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "separator6")) + method separator6 = separator6 + val helpMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "helpMenu")) + method helpMenu = helpMenu + val helpMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast (builder#get_object "helpMenu_menu")) + method helpMenu_menu = helpMenu_menu + val contentsMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "contentsMenuItem")) + method contentsMenuItem = contentsMenuItem + val aboutMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast (builder#get_object "aboutMenuItem")) + method aboutMenuItem = aboutMenuItem + val hbox99 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox99")) + method hbox99 = hbox99 + val hpaneScriptSequent = + new GPack.paned (GtkPack.Paned.cast (builder#get_object "hpaneScriptSequent")) + method hpaneScriptSequent = hpaneScriptSequent + val hbox18 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox18")) + method hbox18 = hbox18 + val tacticsButtonsHandlebox = + new GPack.box (GtkPack.Box.cast (builder#get_object "TacticsButtonsHandlebox")) + method tacticsButtonsHandlebox = tacticsButtonsHandlebox + val vboxTacticsPalette = + new GPack.box (GtkPack.Box.cast (builder#get_object "vboxTacticsPalette")) + method vboxTacticsPalette = vboxTacticsPalette + val expander1 = + new GBin.expander (GtkBin.Expander.cast (builder#get_object "expander1")) + method expander1 = expander1 + val vbox1 = + new GPack.box (GtkPack.Box.cast (builder#get_object "vbox1")) + method vbox1 = vbox1 + val butImpl_intro = + new GButton.button (GtkButton.Button.cast (builder#get_object "butImpl_intro")) + method butImpl_intro = butImpl_intro + val label8 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label8")) + method label8 = label8 + val butAnd_intro = + new GButton.button (GtkButton.Button.cast (builder#get_object "butAnd_intro")) + method butAnd_intro = butAnd_intro + val label7 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label7")) + method label7 = label7 + val butOr_intro_left = + new GButton.button (GtkButton.Button.cast (builder#get_object "butOr_intro_left")) + method butOr_intro_left = butOr_intro_left + val label9 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label9")) + method label9 = label9 + val butOr_intro_right = + new GButton.button (GtkButton.Button.cast (builder#get_object "butOr_intro_right")) + method butOr_intro_right = butOr_intro_right + val label10 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label10")) + method label10 = label10 + val butNot_intro = + new GButton.button (GtkButton.Button.cast (builder#get_object "butNot_intro")) + method butNot_intro = butNot_intro + val label11 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label11")) + method label11 = label11 + val butTop_intro = + new GButton.button (GtkButton.Button.cast (builder#get_object "butTop_intro")) + method butTop_intro = butTop_intro + val label12 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label12")) + method label12 = label12 + val butForall_intro = + new GButton.button (GtkButton.Button.cast (builder#get_object "butForall_intro")) + method butForall_intro = butForall_intro + val label20 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label20")) + method label20 = label20 + val butExists_intro = + new GButton.button (GtkButton.Button.cast (builder#get_object "butExists_intro")) + method butExists_intro = butExists_intro + val label21 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label21")) + method label21 = label21 + val label4 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label4")) + method label4 = label4 + val expander2 = + new GBin.expander (GtkBin.Expander.cast (builder#get_object "expander2")) + method expander2 = expander2 + val vbox3 = + new GPack.box (GtkPack.Box.cast (builder#get_object "vbox3")) + method vbox3 = vbox3 + val butImpl_elim = + new GButton.button (GtkButton.Button.cast (builder#get_object "butImpl_elim")) + method butImpl_elim = butImpl_elim + val label22 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label22")) + method label22 = label22 + val butAnd_elim_left = + new GButton.button (GtkButton.Button.cast (builder#get_object "butAnd_elim_left")) + method butAnd_elim_left = butAnd_elim_left + val label23 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label23")) + method label23 = label23 + val butAnd_elim_right = + new GButton.button (GtkButton.Button.cast (builder#get_object "butAnd_elim_right")) + method butAnd_elim_right = butAnd_elim_right + val label24 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label24")) + method label24 = label24 + val butOr_elim = + new GButton.button (GtkButton.Button.cast (builder#get_object "butOr_elim")) + method butOr_elim = butOr_elim + val label27 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label27")) + method label27 = label27 + val butNot_elim = + new GButton.button (GtkButton.Button.cast (builder#get_object "butNot_elim")) + method butNot_elim = butNot_elim + val label31 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label31")) + method label31 = label31 + val butBot_elim = + new GButton.button (GtkButton.Button.cast (builder#get_object "butBot_elim")) + method butBot_elim = butBot_elim + val label33 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label33")) + method label33 = label33 + val butForall_elim = + new GButton.button (GtkButton.Button.cast (builder#get_object "butForall_elim")) + method butForall_elim = butForall_elim + val label34 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label34")) + method label34 = label34 + val butExists_elim = + new GButton.button (GtkButton.Button.cast (builder#get_object "butExists_elim")) + method butExists_elim = butExists_elim + val label35 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label35")) + method label35 = label35 + val label5 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label5")) + method label5 = label5 + val expander3 = + new GBin.expander (GtkBin.Expander.cast (builder#get_object "expander3")) + method expander3 = expander3 + val vbox4 = + new GPack.box (GtkPack.Box.cast (builder#get_object "vbox4")) + method vbox4 = vbox4 + val butRAA = + new GButton.button (GtkButton.Button.cast (builder#get_object "butRAA")) + method butRAA = butRAA + val butUseLemma = + new GButton.button (GtkButton.Button.cast (builder#get_object "butUseLemma")) + method butUseLemma = butUseLemma + val butDischarge = + new GButton.button (GtkButton.Button.cast (builder#get_object "butDischarge")) + method butDischarge = butDischarge + val label6 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label6")) + method label6 = label6 + val vboxScript = + new GPack.box (GtkPack.Box.cast (builder#get_object "vboxScript")) + method vboxScript = vboxScript + val hbox28 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox28")) + method hbox28 = hbox28 + val buttonsToolbar = + new GButton.toolbar (GtkButton.Toolbar.cast (builder#get_object "buttonsToolbar")) + method buttonsToolbar = buttonsToolbar + val toolitem41 = + new GButton.tool_item (GtkButton.ToolItem.cast (builder#get_object "toolitem41")) + method toolitem41 = toolitem41 + val scriptTopButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "scriptTopButton")) + method scriptTopButton = scriptTopButton + val image920 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image920")) + method image920 = image920 + val toolitem42 = + new GButton.tool_item (GtkButton.ToolItem.cast (builder#get_object "toolitem42")) + method toolitem42 = toolitem42 + val scriptRetractButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "scriptRetractButton")) + method scriptRetractButton = scriptRetractButton + val image921 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image921")) + method image921 = image921 + val toolitem43 = + new GButton.tool_item (GtkButton.ToolItem.cast (builder#get_object "toolitem43")) + method toolitem43 = toolitem43 + val scriptJumpButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "scriptJumpButton")) + method scriptJumpButton = scriptJumpButton + val image922 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image922")) + method image922 = image922 + val toolitem44 = + new GButton.tool_item (GtkButton.ToolItem.cast (builder#get_object "toolitem44")) + method toolitem44 = toolitem44 + val scriptAdvanceButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "scriptAdvanceButton")) + method scriptAdvanceButton = scriptAdvanceButton + val image923 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image923")) + method image923 = image923 + val toolitem45 = + new GButton.tool_item (GtkButton.ToolItem.cast (builder#get_object "toolitem45")) + method toolitem45 = toolitem45 + val scriptBottomButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "scriptBottomButton")) + method scriptBottomButton = scriptBottomButton + val image924 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image924")) + method image924 = image924 + val toolbar2 = + new GButton.toolbar (GtkButton.Toolbar.cast (builder#get_object "toolbar2")) + method toolbar2 = toolbar2 + val toolitem46 = + new GButton.tool_item (GtkButton.ToolItem.cast (builder#get_object "toolitem46")) + method toolitem46 = toolitem46 + val scriptAbortButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "scriptAbortButton")) + method scriptAbortButton = scriptAbortButton + val image927 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image927")) + method image927 = image927 + val scriptNotebook = + new GPack.notebook (GtkPack.Notebook.cast (builder#get_object "scriptNotebook")) + method scriptNotebook = scriptNotebook + val vpaned1 = + new GPack.paned (GtkPack.Paned.cast (builder#get_object "vpaned1")) + method vpaned1 = vpaned1 + val sequentsNotebook = + new GPack.notebook (GtkPack.Notebook.cast (builder#get_object "sequentsNotebook")) + method sequentsNotebook = sequentsNotebook + val hbox9 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox9")) + method hbox9 = hbox9 + val logScrolledWin = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "logScrolledWin")) + method logScrolledWin = logScrolledWin + val logTextView = + new GText.view (GtkText.View.cast (builder#get_object "logTextView")) + method logTextView = logTextView + val hbox10 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox10")) + method hbox10 = hbox10 + val statusBar = + new GMisc.statusbar (GtkMisc.Statusbar.cast (builder#get_object "StatusBar")) + method statusBar = statusBar + val hintNotebook = + new GPack.notebook (GtkPack.Notebook.cast (builder#get_object "HintNotebook")) + method hintNotebook = hintNotebook + val hintLowImage = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "HintLowImage")) + method hintLowImage = hintLowImage + val label14 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label14")) + method label14 = label14 + val hintMediumImage = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "HintMediumImage")) + method hintMediumImage = hintMediumImage + val label15 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label15")) + method label15 = label15 + val hintHighImage = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "HintHighImage")) + method hintHighImage = hintHighImage + val label16 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label16")) + method label16 = label16 + method reparent parent = + mainWinEventBox#misc#reparent parent; + toplevel#destroy () + end +class uriChoiceDialog ?translation_domain () = + let builder = GBuilder.builder ?translation_domain () in + let _ = builder#add_objects_from_string data ["UriChoiceDialog"] in + object + val toplevel = + new GWindow.dialog_any (GtkWindow.Dialog.cast (builder#get_object "UriChoiceDialog")) + method toplevel = toplevel + val uriChoiceDialog = + new GWindow.dialog_any (GtkWindow.Dialog.cast (builder#get_object "UriChoiceDialog")) + method uriChoiceDialog = uriChoiceDialog + val dialog_vbox3 = + new GPack.box (GtkPack.Box.cast (builder#get_object "dialog-vbox3")) + method dialog_vbox3 = dialog_vbox3 + val dialog_action_area3 = + new GPack.button_box (GtkPack.BBox.cast (builder#get_object "dialog-action_area3")) + method dialog_action_area3 = dialog_action_area3 + val uriChoiceAbortButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "UriChoiceAbortButton")) + method uriChoiceAbortButton = uriChoiceAbortButton + val uriChoiceSelectedButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "UriChoiceSelectedButton")) + method uriChoiceSelectedButton = uriChoiceSelectedButton + val alignment2 = + new GBin.alignment (GtkBin.Alignment.cast (builder#get_object "alignment2")) + method alignment2 = alignment2 + val hbox3 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox3")) + method hbox3 = hbox3 + val image19 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image19")) + method image19 = image19 + val label3 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label3")) + method label3 = label3 + val uriChoiceConstantsButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "UriChoiceConstantsButton")) + method uriChoiceConstantsButton = uriChoiceConstantsButton + val copyButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "copyButton")) + method copyButton = copyButton + val uriChoiceAutoButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "uriChoiceAutoButton")) + method uriChoiceAutoButton = uriChoiceAutoButton + val alignment5 = + new GBin.alignment (GtkBin.Alignment.cast (builder#get_object "alignment5")) + method alignment5 = alignment5 + val hbox16 = + new GPack.box (GtkPack.Box.cast (builder#get_object "hbox16")) + method hbox16 = hbox16 + val image302 = + new GMisc.image (GtkMisc.Image.cast (builder#get_object "image302")) + method image302 = image302 + val okLabel = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "okLabel")) + method okLabel = okLabel + val uriChoiceForwardButton = + new GButton.button (GtkButton.Button.cast (builder#get_object "uriChoiceForwardButton")) + method uriChoiceForwardButton = uriChoiceForwardButton + val vbox2 = + new GPack.box (GtkPack.Box.cast (builder#get_object "vbox2")) + method vbox2 = vbox2 + val uriChoiceLabel = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "UriChoiceLabel")) + method uriChoiceLabel = uriChoiceLabel + val scrolledwindow1 = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (builder#get_object "scrolledwindow1")) + method scrolledwindow1 = scrolledwindow1 + val uriChoiceTreeView = + new GTree.view (GtkTree.TreeView.cast (builder#get_object "UriChoiceTreeView")) + method uriChoiceTreeView = uriChoiceTreeView + val uriEntryHBox = + new GPack.box (GtkPack.Box.cast (builder#get_object "uriEntryHBox")) + method uriEntryHBox = uriEntryHBox + val label2 = + new GMisc.label (GtkMisc.Label.cast (builder#get_object "label2")) + method label2 = label2 + val entry1 = + new GEdit.entry (GtkEdit.Entry.cast (builder#get_object "entry1")) + method entry1 = entry1 + method reparent parent = + dialog_vbox3#misc#reparent parent; + toplevel#destroy () + end