]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 9bd8f35)
Remove all traces of autoconf/automake/makefile
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Jan 2023 17:59:47 +0000 (18:59 +0100)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 14 Feb 2023 14:23:41 +0000 (15:23 +0100)
- also fixes installation of help/C files to include only .xml files
  and figures

12 files changed:
.gitignore patch | blob | history
matita/.merlin [deleted file] patch | blob | history
matita/Makefile [deleted file] patch | blob | history
matita/Makefile.defs.in [deleted file] patch | blob | history
matita/components/Makefile [deleted file] patch | blob | history
matita/components/Makefile.common [deleted file] patch | blob | history
matita/configure.ac [deleted file] patch | blob | history
matita/matita.install patch | blob | history
matita/matita/Makefile [deleted file] patch | blob | history
matita/matita/dune patch | blob | history
matita/matita/help/C/matita.pdf patch | blob | history
matita/matita/matitaGeneratedGui.ml [new file with mode: 0644] patch | blob

diff --git a/.gitignore b/.gitignore
index 7ad5d443daa67bee2c13da24aa94ca3bb445ccdc..d2e1e23e52b91581c12ad4d6b53fef8bc804f980 100644 (file)
--- 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 (file)
index 92f60a6..0000000
--- 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 (file)
index 2080917..0000000
--- 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 (file)
index 90a203f..0000000
--- 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 (file)
index f30f284..0000000
--- 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 (file)
index 0c61faa..0000000
--- 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 (file)
index cf8a8e4..0000000
--- 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 d8d93e4e89584ac3a939df61abdc28e9e9abe8cb..b1007b300c18a345f9d886e060257a6cafc6426b 100644 (file)
--- 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 (file)
index c0a7903..0000000
--- 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 f1798f02010ebb73275fa5efbcc0646eba40c5da..4f01419161f723712c9e08adafb02c25daf6cc50 100644 (file)
--- 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 78a10f2a329b38dedae1ce00e160e604edf6e7e0..ca672325848c53a4c5ba462e9eb26480fc3c3ddf 100644 (file)
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 (file)
index 0000000..390f079
--- /dev/null
+++ b/matita/matita/matitaGeneratedGui.ml
@@ -0,0 +1,880 @@
+(* Automatically generated from matita.ui by lablgladecc *)
+
+let data = "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n<!-- Generated with glade 3.22.1 -->\n<interface>\n  <requires lib=\"gtk+\" version=\"3.20\"/>\n  <object class=\"GtkWindow\" id=\"AutoWin\">\n    <property name=\"width_request\">600</property>\n    <property name=\"height_request\">400</property>\n    <property name=\"visible\">True</property>\n    <property name=\"can_focus\">False</property>\n    <property name=\"title\" translatable=\"yes\">Auto</property>\n    <property name=\"type_hint\">dialog</property>\n    <property name=\"gravity\">south-east</property>\n    <child>\n      <object class=\"GtkBox\" id=\"vbox17\">\n        <property name=\"visible\">True</property>\n        <property name=\"can_focus\">False</property>\n        <property name=\"orientation\">vertical</property>\n        <child>\n          <object class=\"GtkBox\" id=\"hbox30\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"spacing\">2</property>\n            <child>\n              <object class=\"GtkScrolledWindow\" id=\"scrolledwindowAREA\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"shadow_type\">in</property>\n                <child>\n                  <object class=\"GtkViewport\" id=\"viewportAREA\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <child>\n                      <object class=\"GtkGrid\" id=\"table\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkBox\" id=\"vbox18\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"orientation\">vertical</property>\n                <child>\n                  <object class=\"GtkButton\" id=\"buttonUP\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"receives_default\">False</property>\n                    <child>\n                      <object class=\"GtkAlignment\" id=\"alignment19\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"xscale\">0</property>\n                        <property name=\"yscale\">0</property>\n                        <child>\n                          <object class=\"GtkBox\" id=\"hbox31\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"spacing\">2</property>\n                            <child>\n                              <object class=\"GtkImage\" id=\"image1066\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">False</property>\n                                <property name=\"stock\">gtk-go-up</property>\n                              </object>\n                              <packing>\n                                <property name=\"expand\">False</property>\n                                <property name=\"fill\">False</property>\n                                <property name=\"position\">0</property>\n                              </packing>\n                            </child>\n                            <child>\n                              <object class=\"GtkLabel\" id=\"label30\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">False</property>\n                                <property name=\"use_underline\">True</property>\n                              </object>\n                              <packing>\n                                <property name=\"expand\">False</property>\n                                <property name=\"fill\">False</property>\n                                <property name=\"position\">1</property>\n                              </packing>\n                            </child>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">True</property>\n                    <property name=\"fill\">True</property>\n                    <property name=\"position\">0</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkButton\" id=\"buttonDOWN\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"receives_default\">False</property>\n                    <child>\n                      <object class=\"GtkImage\" id=\"image1065\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"stock\">gtk-go-down</property>\n                      </object>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">True</property>\n                    <property name=\"fill\">True</property>\n                    <property name=\"position\">1</property>\n                  </packing>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n          </object>\n          <packing>\n            <property name=\"expand\">True</property>\n            <property name=\"fill\">True</property>\n            <property name=\"position\">0</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkSeparator\" id=\"hseparator3\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n          </object>\n          <packing>\n            <property name=\"expand\">False</property>\n            <property name=\"fill\">True</property>\n            <property name=\"padding\">3</property>\n            <property name=\"position\">1</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkBox\" id=\"hbox32\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <child>\n              <object class=\"GtkLabel\" id=\"labelLAST\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"label\" translatable=\"yes\">Last:</property>\n                <property name=\"xalign\">0</property>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButtonBox\" id=\"hbuttonbox3\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"border_width\">4</property>\n                <property name=\"spacing\">4</property>\n                <property name=\"layout_style\">end</property>\n                <child>\n                  <object class=\"GtkButton\" id=\"buttonPAUSE\">\n                    <property name=\"label\">gtk-media-pause</property>\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"can_default\">True</property>\n                    <property name=\"receives_default\">False</property>\n                    <property name=\"use_stock\">True</property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">False</property>\n                    <property name=\"fill\">False</property>\n                    <property name=\"position\">0</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkButton\" id=\"buttonPLAY\">\n                    <property name=\"label\">gtk-media-play</property>\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"can_default\">True</property>\n                    <property name=\"receives_default\">False</property>\n                    <property name=\"use_stock\">True</property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">False</property>\n                    <property name=\"fill\">False</property>\n                    <property name=\"position\">1</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkButton\" id=\"buttonNEXT\">\n                    <property name=\"label\">gtk-media-next</property>\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"can_default\">True</property>\n                    <property name=\"receives_default\">False</property>\n                    <property name=\"use_stock\">True</property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">False</property>\n                    <property name=\"fill\">False</property>\n                    <property name=\"position\">2</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkButton\" id=\"buttonCLOSE\">\n                    <property name=\"label\">gtk-close</property>\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"can_default\">True</property>\n                    <property name=\"receives_default\">False</property>\n                    <property name=\"use_stock\">True</property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">False</property>\n                    <property name=\"fill\">False</property>\n                    <property name=\"position\">3</property>\n                  </packing>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n          </object>\n          <packing>\n            <property name=\"expand\">False</property>\n            <property name=\"fill\">True</property>\n            <property name=\"position\">2</property>\n          </packing>\n        </child>\n      </object>\n    </child>\n  </object>\n  <object class=\"GtkWindow\" id=\"BrowserWin\">\n    <property name=\"width_request\">500</property>\n    <property name=\"height_request\">480</property>\n    <property name=\"visible\">True</property>\n    <property name=\"can_focus\">False</property>\n    <property name=\"title\" translatable=\"yes\">Cic browser</property>\n    <property name=\"window_position\">center-on-parent</property>\n    <property name=\"default_width\">500</property>\n    <property name=\"default_height\">480</property>\n    <property name=\"destroy_with_parent\">True</property>\n    <child>\n      <object class=\"GtkEventBox\" id=\"BrowserWinEventBox\">\n        <property name=\"visible\">True</property>\n        <property name=\"can_focus\">False</property>\n        <child>\n          <object class=\"GtkBox\" id=\"BrowserVBox\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"orientation\">vertical</property>\n            <child>\n              <object class=\"GtkMenuBar\" id=\"menubar2\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"BrowserFileMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_File</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"BrowserFileMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"BrowserNewMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_New</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"BrowserUrlMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Open _Location ...</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"L\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separatormenuitem1\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"BrowserCloseMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Quit</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"BrowserEditMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_Edit</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"BrowserEditMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"BrowserCopyMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Copy</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkFrame\" id=\"frame2\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"label_xalign\">0</property>\n                <property name=\"label_yalign\">0</property>\n                <property name=\"shadow_type\">none</property>\n                <child>\n                  <object class=\"GtkBox\" id=\"BrowserHBox\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <child>\n                      <object class=\"GtkButton\" id=\"BrowserNewButton\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"receives_default\">False</property>\n                        <property name=\"relief\">none</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image303\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-new</property>\n                          </object>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">False</property>\n                        <property name=\"position\">0</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkButton\" id=\"BrowserBackButton\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"receives_default\">False</property>\n                        <property name=\"relief\">none</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image304\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-go-back</property>\n                          </object>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">False</property>\n                        <property name=\"position\">1</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkButton\" id=\"BrowserForwardButton\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"receives_default\">False</property>\n                        <property name=\"relief\">none</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image305\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-go-forward</property>\n                          </object>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">False</property>\n                        <property name=\"position\">2</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkButton\" id=\"BrowserRefreshButton\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"can_default\">True</property>\n                        <property name=\"receives_default\">False</property>\n                        <property name=\"tooltip_text\" translatable=\"yes\">refresh</property>\n                        <property name=\"relief\">none</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image229\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-refresh</property>\n                          </object>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">False</property>\n                        <property name=\"position\">3</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkButton\" id=\"BrowserHomeButton\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"can_default\">True</property>\n                        <property name=\"receives_default\">False</property>\n                        <property name=\"tooltip_text\" translatable=\"yes\">home</property>\n                        <property name=\"relief\">none</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image190\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-home</property>\n                          </object>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">False</property>\n                        <property name=\"position\">4</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkImage\" id=\"image301\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"stock\">gtk-jump-to</property>\n                        <property name=\"icon_size\">2</property>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">False</property>\n                        <property name=\"padding\">3</property>\n                        <property name=\"position\">5</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkBox\" id=\"UriHBox\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkEntry\" id=\"browserUri\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">True</property>\n                            <property name=\"has_focus\">True</property>\n                            <property name=\"invisible_char\">\226\151\143</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">True</property>\n                            <property name=\"fill\">True</property>\n                            <property name=\"position\">0</property>\n                          </packing>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">True</property>\n                        <property name=\"fill\">True</property>\n                        <property name=\"position\">6</property>\n                      </packing>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkNotebook\" id=\"mathOrListNotebook\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <child>\n                  <object class=\"GtkScrolledWindow\" id=\"ScrolledBrowser\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                  </object>\n                </child>\n                <child type=\"tab\">\n                  <object class=\"GtkLabel\" id=\"mathLabel\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">MathView</property>\n                  </object>\n                  <packing>\n                    <property name=\"tab_fill\">False</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkScrolledWindow\" id=\"scrolledwindow9\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"shadow_type\">in</property>\n                    <child>\n                      <object class=\"GtkTreeView\" id=\"whelpResultTreeview\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"headers_visible\">False</property>\n                        <child internal-child=\"selection\">\n                          <object class=\"GtkTreeSelection\"/>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"position\">1</property>\n                  </packing>\n                </child>\n                <child type=\"tab\">\n                  <object class=\"GtkLabel\" id=\"WhelpResult\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">WhelpResult</property>\n                  </object>\n                  <packing>\n                    <property name=\"position\">1</property>\n                    <property name=\"tab_fill\">False</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkScrolledWindow\" id=\"scrolledwindow11\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <child>\n                      <object class=\"GtkViewport\" id=\"viewport2\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"shadow_type\">none</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"BrowserImage\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-missing-image</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"position\">2</property>\n                  </packing>\n                </child>\n                <child type=\"tab\">\n                  <object class=\"GtkLabel\" id=\"EasterEggLabel\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">WhelpEasterEgg</property>\n                  </object>\n                  <packing>\n                    <property name=\"position\">2</property>\n                    <property name=\"tab_fill\">False</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkScrolledWindow\" id=\"GraphScrolledWin\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                  </object>\n                  <packing>\n                    <property name=\"position\">3</property>\n                  </packing>\n                </child>\n                <child type=\"tab\">\n                  <object class=\"GtkLabel\" id=\"label26\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">Graph</property>\n                  </object>\n                  <packing>\n                    <property name=\"position\">3</property>\n                    <property name=\"tab_fill\">False</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkBox\" id=\"vbox20\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"orientation\">vertical</property>\n                    <child>\n                      <object class=\"GtkScrolledWindow\" id=\"scrolledwinContent\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"border_width\">3</property>\n                        <property name=\"shadow_type\">in</property>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">True</property>\n                        <property name=\"fill\">True</property>\n                        <property name=\"position\">0</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkBox\" id=\"hbox35\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"border_width\">4</property>\n                        <property name=\"spacing\">4</property>\n                        <child>\n                          <object class=\"GtkBox\" id=\"vbox22\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"orientation\">vertical</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">True</property>\n                            <property name=\"fill\">True</property>\n                            <property name=\"position\">0</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkEntry\" id=\"entrySearch\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">True</property>\n                            <property name=\"has_focus\">True</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">True</property>\n                            <property name=\"fill\">True</property>\n                            <property name=\"position\">1</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkButton\" id=\"buttonSearch\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">True</property>\n                            <property name=\"receives_default\">False</property>\n                            <child>\n                              <object class=\"GtkAlignment\" id=\"alignment21\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">False</property>\n                                <property name=\"xscale\">0</property>\n                                <property name=\"yscale\">0</property>\n                                <child>\n                                  <object class=\"GtkBox\" id=\"hbox36\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">False</property>\n                                    <property name=\"spacing\">2</property>\n                                    <child>\n                                      <object class=\"GtkImage\" id=\"image1068\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"stock\">gtk-find</property>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"fill\">False</property>\n                                        <property name=\"position\">0</property>\n                                      </packing>\n                                    </child>\n                                    <child>\n                                      <object class=\"GtkLabel\" id=\"label32\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"label\" translatable=\"yes\">Search</property>\n                                        <property name=\"use_underline\">True</property>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"fill\">False</property>\n                                        <property name=\"position\">1</property>\n                                      </packing>\n                                    </child>\n                                  </object>\n                                </child>\n                              </object>\n                            </child>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">2</property>\n                          </packing>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"expand\">False</property>\n                        <property name=\"fill\">True</property>\n                        <property name=\"position\">1</property>\n                      </packing>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"position\">4</property>\n                  </packing>\n                </child>\n                <child type=\"tab\">\n                  <object class=\"GtkLabel\" id=\"SearchText\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">SearchText</property>\n                  </object>\n                  <packing>\n                    <property name=\"position\">4</property>\n                    <property name=\"tab_fill\">False</property>\n                  </packing>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">3</property>\n              </packing>\n            </child>\n          </object>\n        </child>\n      </object>\n    </child>\n  </object>\n  <object class=\"GtkDialog\" id=\"DisambiguationErrors\">\n    <property name=\"width_request\">450</property>\n    <property name=\"height_request\">400</property>\n    <property name=\"can_focus\">False</property>\n    <property name=\"title\" translatable=\"yes\">title</property>\n    <property name=\"modal\">True</property>\n    <property name=\"type_hint\">dialog</property>\n    <child internal-child=\"vbox\">\n      <object class=\"GtkBox\" id=\"vbox14\">\n        <property name=\"visible\">True</property>\n        <property name=\"can_focus\">False</property>\n        <property name=\"orientation\">vertical</property>\n        <child internal-child=\"action_area\">\n          <object class=\"GtkButtonBox\" id=\"hbuttonbox2\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"layout_style\">spread</property>\n          </object>\n          <packing>\n            <property name=\"expand\">False</property>\n            <property name=\"fill\">False</property>\n            <property name=\"pack_type\">end</property>\n            <property name=\"position\">0</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkBox\" id=\"vbox15\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"orientation\">vertical</property>\n            <child>\n              <object class=\"GtkLabel\" id=\"disambiguationErrorsLabel\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"label\" translatable=\"yes\">some informative message here ...</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkScrolledWindow\" id=\"scrolledwindow12\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"vexpand\">True</property>\n                <property name=\"shadow_type\">in</property>\n                <child>\n                  <object class=\"GtkTreeView\" id=\"treeview\">\n                    <property name=\"height_request\">717</property>\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"headers_visible\">False</property>\n                    <child internal-child=\"selection\">\n                      <object class=\"GtkTreeSelection\"/>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n          </object>\n          <packing>\n            <property name=\"expand\">False</property>\n            <property name=\"fill\">True</property>\n            <property name=\"position\">2</property>\n          </packing>\n        </child>\n      </object>\n    </child>\n  </object>\n  <object class=\"GtkWindow\" id=\"FindReplWin\">\n    <property name=\"can_focus\">False</property>\n    <property name=\"border_width\">5</property>\n    <property name=\"title\" translatable=\"yes\">Find &amp; Replace</property>\n    <property name=\"resizable\">False</property>\n    <property name=\"window_position\">mouse</property>\n    <property name=\"type_hint\">dialog</property>\n    <child>\n      <object class=\"GtkGrid\" id=\"table1\">\n        <property name=\"visible\">True</property>\n        <property name=\"can_focus\">False</property>\n        <property name=\"row_spacing\">9</property>\n        <child>\n          <object class=\"GtkLabel\" id=\"label17\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"label\" translatable=\"yes\">Find:</property>\n            <property name=\"xalign\">0</property>\n          </object>\n          <packing>\n            <property name=\"left_attach\">0</property>\n            <property name=\"top_attach\">0</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkLabel\" id=\"label18\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"label\" translatable=\"yes\">Replace with: </property>\n            <property name=\"xalign\">0</property>\n          </object>\n          <packing>\n            <property name=\"left_attach\">0</property>\n            <property name=\"top_attach\">1</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkEntry\" id=\"findEntry\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">True</property>\n            <property name=\"can_default\">True</property>\n            <property name=\"has_default\">True</property>\n          </object>\n          <packing>\n            <property name=\"left_attach\">1</property>\n            <property name=\"top_attach\">0</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkEntry\" id=\"replaceEntry\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">True</property>\n          </object>\n          <packing>\n            <property name=\"left_attach\">1</property>\n            <property name=\"top_attach\">1</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkBox\" id=\"hbox19\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"spacing\">5</property>\n            <property name=\"homogeneous\">True</property>\n            <child>\n              <object class=\"GtkButton\" id=\"findButton\">\n                <property name=\"label\">gtk-find</property>\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"receives_default\">False</property>\n                <property name=\"use_stock\">True</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"findReplButton\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"receives_default\">False</property>\n                <child>\n                  <object class=\"GtkAlignment\" id=\"alignment13\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"xscale\">0</property>\n                    <property name=\"yscale\">0</property>\n                    <child>\n                      <object class=\"GtkBox\" id=\"hbox20\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"spacing\">2</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image357\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-find-and-replace</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">0</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkLabel\" id=\"label19\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Replace</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">1</property>\n                          </packing>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">2</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"cancelButton\">\n                <property name=\"label\">gtk-cancel</property>\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"receives_default\">False</property>\n                <property name=\"use_stock\">True</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">3</property>\n              </packing>\n            </child>\n          </object>\n          <packing>\n            <property name=\"left_attach\">0</property>\n            <property name=\"top_attach\">2</property>\n            <property name=\"width\">2</property>\n          </packing>\n        </child>\n      </object>\n    </child>\n  </object>\n  <object class=\"GtkWindow\" id=\"MainWin\">\n    <property name=\"can_focus\">False</property>\n    <property name=\"title\" translatable=\"yes\">Matita</property>\n    <child>\n      <object class=\"GtkEventBox\" id=\"MainWinEventBox\">\n        <property name=\"visible\">True</property>\n        <property name=\"can_focus\">False</property>\n        <child>\n          <object class=\"GtkBox\" id=\"vbox8\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"orientation\">vertical</property>\n            <child>\n              <object class=\"GtkMenuBar\" id=\"menubar1\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"fileMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_File</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"fileMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"newMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_New</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"n\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"openMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Open...</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"o\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"saveMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Save</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"s\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"saveAsMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Save as...</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"s\" signal=\"activate\" modifiers=\"GDK_SHIFT_MASK | GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator2\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"closeMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Close</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"w\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"quitMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Quit</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"q\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"editMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_Edit</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"editMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"undoMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"sensitive\">False</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Undo</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"z\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"redoMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"sensitive\">False</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">_Redo</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"z\" signal=\"activate\" modifiers=\"GDK_SHIFT_MASK | GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator3\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"cutMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Cut</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"x\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"copyMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Copy</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"c\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"pasteMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Paste</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"v\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"pastePatternMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Paste as pattern</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkCheckMenuItem\" id=\"unicodeAsTexMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Paste Unicode as TeX</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkCheckMenuItem\" id=\"menuitemAutoAltL\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Auto-expand TeX Macros</property>\n                            <property name=\"use_underline\">True</property>\n                            <property name=\"active\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"deleteMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Delete</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator4\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"selectAllMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Select _All</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator7\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"findReplMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Find and replace...</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"f\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator8\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"LigatureButton\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Next ligature</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"l\" signal=\"activate\" modifiers=\"GDK_MOD1_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"externalEditorMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Edit with e_xternal editor</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"scriptMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_Script</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"scriptMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"scriptAdvanceMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Execute 1 phrase</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"Page_Down\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK | GDK_MOD1_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"scriptRetractMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Retract 1 phrase</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"Page_Up\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK | GDK_MOD1_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator9\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"scriptBottomMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Execute all</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"End\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK | GDK_MOD1_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"scriptTopMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Retract all</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"Home\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK | GDK_MOD1_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator10\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"scriptJumpMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Execute until cursor</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"period\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK | GDK_MOD1_MASK\"/>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"viewMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_View</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"viewMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"newCicBrowserMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">New CIC _browser</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"F3\" signal=\"activate\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator5\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkCheckMenuItem\" id=\"fullscreenMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">_Fullscreen</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"F11\" signal=\"activate\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkCheckMenuItem\" id=\"menuitemPalette\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Natural deduction palette</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"F2\" signal=\"activate\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator1\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"increaseFontSizeMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Zoom in</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"plus\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"decreaseFontSizeMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Zoom out</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"minus\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"normalFontSizeMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Normal size</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"equal\" signal=\"activate\" modifiers=\"GDK_CONTROL_MASK\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator12\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkCheckMenuItem\" id=\"ppNotationMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Pretty print notation</property>\n                            <property name=\"use_underline\">True</property>\n                            <property name=\"active\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkCheckMenuItem\" id=\"hideCoercionsMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Hide coercions</property>\n                            <property name=\"use_underline\">True</property>\n                            <property name=\"active\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator13\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"showCoercionsGraphMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Coercions Graph</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"showHintsDbMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Hints database</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"showTermGrammarMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Terms grammar</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"showUnicodeTable\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">TeX/UTF-8 table</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"debugMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_Debug</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"debugMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkSeparatorMenuItem\" id=\"separator6\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n                <child>\n                  <object class=\"GtkMenuItem\" id=\"helpMenu\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">_Help</property>\n                    <property name=\"use_underline\">True</property>\n                    <child type=\"submenu\">\n                      <object class=\"GtkMenu\" id=\"helpMenu_menu\">\n                        <property name=\"can_focus\">False</property>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"contentsMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">Contents</property>\n                            <property name=\"use_underline\">True</property>\n                            <accelerator key=\"F1\" signal=\"activate\"/>\n                          </object>\n                        </child>\n                        <child>\n                          <object class=\"GtkMenuItem\" id=\"aboutMenuItem\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\">About</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkBox\" id=\"hbox99\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <child>\n                  <object class=\"GtkPaned\" id=\"hpaneScriptSequent\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <child>\n                      <object class=\"GtkBox\" id=\"hbox18\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"spacing\">2</property>\n                        <child>\n                          <object class=\"GtkBox\" id=\"TacticsButtonsHandlebox\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <child>\n                              <object class=\"GtkBox\" id=\"vboxTacticsPalette\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">False</property>\n                                <property name=\"orientation\">vertical</property>\n                                <child>\n                                  <object class=\"GtkExpander\" id=\"expander1\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">True</property>\n                                    <child>\n                                      <object class=\"GtkBox\" id=\"vbox1\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"orientation\">vertical</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butImpl_intro\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label8\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Implication (\226\135\146&lt;sub&gt;i&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">0</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butAnd_intro\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label7\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Conjunction (\226\136\167&lt;sub&gt;i&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">1</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butOr_intro_left\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label9\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Disjunction left (\226\136\168&lt;sub&gt;i-l&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">2</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butOr_intro_right\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label10\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Disjunction right (\226\136\168&lt;sub&gt;i-r&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">3</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butNot_intro\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label11\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Negation (\194\172&lt;sub&gt;i&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">4</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butTop_intro\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label12\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Top (\226\138\164&lt;sub&gt;i&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">5</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butForall_intro\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label20\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Universal (\226\136\128&lt;sub&gt;i&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">6</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butExists_intro\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label21\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Existential (\226\136\131&lt;sub&gt;i&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">7</property>\n                                          </packing>\n                                        </child>\n                                      </object>\n                                    </child>\n                                    <child type=\"label\">\n                                      <object class=\"GtkLabel\" id=\"label4\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"label\" translatable=\"yes\">Introduction rules</property>\n                                      </object>\n                                    </child>\n                                  </object>\n                                  <packing>\n                                    <property name=\"expand\">False</property>\n                                    <property name=\"fill\">True</property>\n                                    <property name=\"position\">0</property>\n                                  </packing>\n                                </child>\n                                <child>\n                                  <object class=\"GtkExpander\" id=\"expander2\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">True</property>\n                                    <child>\n                                      <object class=\"GtkBox\" id=\"vbox3\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"orientation\">vertical</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butImpl_elim\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label22\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Implication (\226\135\146&lt;sub&gt;e&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">0</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butAnd_elim_left\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label23\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Conjunction left (\226\136\167&lt;sub&gt;e-l&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">1</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butAnd_elim_right\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label24\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Conjunction right (\226\136\167&lt;sub&gt;e-r&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">2</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butOr_elim\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label27\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Disjunction (\226\136\168&lt;sub&gt;e&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">3</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butNot_elim\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label31\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Negation (\194\172&lt;sub&gt;e&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">4</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butBot_elim\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label33\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Bottom (\226\138\165&lt;sub&gt;e&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">5</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butForall_elim\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label34\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Universal (\226\136\128&lt;sub&gt;e&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">6</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butExists_elim\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                            <child>\n                                              <object class=\"GtkLabel\" id=\"label35\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"label\" translatable=\"yes\">Existential (\226\136\131&lt;sub&gt;e&lt;/sub&gt;)</property>\n                                                <property name=\"use_markup\">True</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">7</property>\n                                          </packing>\n                                        </child>\n                                      </object>\n                                    </child>\n                                    <child type=\"label\">\n                                      <object class=\"GtkLabel\" id=\"label5\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"label\" translatable=\"yes\">Elimination rules</property>\n                                      </object>\n                                    </child>\n                                  </object>\n                                  <packing>\n                                    <property name=\"expand\">False</property>\n                                    <property name=\"fill\">True</property>\n                                    <property name=\"position\">1</property>\n                                  </packing>\n                                </child>\n                                <child>\n                                  <object class=\"GtkExpander\" id=\"expander3\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">True</property>\n                                    <child>\n                                      <object class=\"GtkBox\" id=\"vbox4\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"orientation\">vertical</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butRAA\">\n                                            <property name=\"label\" translatable=\"yes\">Reduction to Absurdity (RAA)</property>\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">0</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butUseLemma\">\n                                            <property name=\"label\" translatable=\"yes\">Use lemma (lem)</property>\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">1</property>\n                                          </packing>\n                                        </child>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"butDischarge\">\n                                            <property name=\"label\" translatable=\"yes\">Discharge (discharge)</property>\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">True</property>\n                                          </object>\n                                          <packing>\n                                            <property name=\"expand\">True</property>\n                                            <property name=\"fill\">True</property>\n                                            <property name=\"position\">2</property>\n                                          </packing>\n                                        </child>\n                                      </object>\n                                    </child>\n                                    <child type=\"label\">\n                                      <object class=\"GtkLabel\" id=\"label6\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <property name=\"label\" translatable=\"yes\">Misc rules</property>\n                                      </object>\n                                    </child>\n                                  </object>\n                                  <packing>\n                                    <property name=\"expand\">False</property>\n                                    <property name=\"fill\">True</property>\n                                    <property name=\"position\">2</property>\n                                  </packing>\n                                </child>\n                              </object>\n                              <packing>\n                                <property name=\"expand\">False</property>\n                                <property name=\"fill\">True</property>\n                                <property name=\"position\">0</property>\n                              </packing>\n                            </child>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">True</property>\n                            <property name=\"position\">0</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkBox\" id=\"vboxScript\">\n                            <property name=\"width_request\">400</property>\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"orientation\">vertical</property>\n                            <child>\n                              <object class=\"GtkBox\" id=\"hbox28\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">False</property>\n                                <child>\n                                  <object class=\"GtkToolbar\" id=\"buttonsToolbar\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">False</property>\n                                    <property name=\"toolbar_style\">both</property>\n                                    <child>\n                                      <object class=\"GtkToolItem\" id=\"toolitem41\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"scriptTopButton\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">False</property>\n                                            <property name=\"tooltip_text\" translatable=\"yes\">Retract all</property>\n                                            <property name=\"relief\">none</property>\n                                            <child>\n                                              <object class=\"GtkImage\" id=\"image920\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"stock\">gtk-goto-top</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                        </child>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"homogeneous\">False</property>\n                                      </packing>\n                                    </child>\n                                    <child>\n                                      <object class=\"GtkToolItem\" id=\"toolitem42\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"scriptRetractButton\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">False</property>\n                                            <property name=\"tooltip_text\" translatable=\"yes\">Retract 1 phrase</property>\n                                            <property name=\"relief\">none</property>\n                                            <child>\n                                              <object class=\"GtkImage\" id=\"image921\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"stock\">gtk-go-up</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                        </child>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"homogeneous\">False</property>\n                                      </packing>\n                                    </child>\n                                    <child>\n                                      <object class=\"GtkToolItem\" id=\"toolitem43\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"scriptJumpButton\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">False</property>\n                                            <property name=\"tooltip_text\" translatable=\"yes\">Execute until cursor</property>\n                                            <property name=\"relief\">none</property>\n                                            <child>\n                                              <object class=\"GtkImage\" id=\"image922\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"stock\">gtk-jump-to</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                        </child>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"homogeneous\">False</property>\n                                      </packing>\n                                    </child>\n                                    <child>\n                                      <object class=\"GtkToolItem\" id=\"toolitem44\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"scriptAdvanceButton\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">False</property>\n                                            <property name=\"tooltip_text\" translatable=\"yes\">Execute 1 phrase</property>\n                                            <property name=\"relief\">none</property>\n                                            <child>\n                                              <object class=\"GtkImage\" id=\"image923\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"stock\">gtk-go-down</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                        </child>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"homogeneous\">False</property>\n                                      </packing>\n                                    </child>\n                                    <child>\n                                      <object class=\"GtkToolItem\" id=\"toolitem45\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"scriptBottomButton\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">False</property>\n                                            <property name=\"tooltip_text\" translatable=\"yes\">Execute all</property>\n                                            <property name=\"relief\">none</property>\n                                            <child>\n                                              <object class=\"GtkImage\" id=\"image924\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"stock\">gtk-goto-bottom</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                        </child>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"homogeneous\">False</property>\n                                      </packing>\n                                    </child>\n                                  </object>\n                                  <packing>\n                                    <property name=\"expand\">True</property>\n                                    <property name=\"fill\">True</property>\n                                    <property name=\"position\">0</property>\n                                  </packing>\n                                </child>\n                                <child>\n                                  <object class=\"GtkToolbar\" id=\"toolbar2\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">False</property>\n                                    <property name=\"orientation\">vertical</property>\n                                    <property name=\"toolbar_style\">both</property>\n                                    <child>\n                                      <object class=\"GtkToolItem\" id=\"toolitem46\">\n                                        <property name=\"visible\">True</property>\n                                        <property name=\"can_focus\">False</property>\n                                        <child>\n                                          <object class=\"GtkButton\" id=\"scriptAbortButton\">\n                                            <property name=\"visible\">True</property>\n                                            <property name=\"can_focus\">True</property>\n                                            <property name=\"receives_default\">False</property>\n                                            <property name=\"relief\">none</property>\n                                            <child>\n                                              <object class=\"GtkImage\" id=\"image927\">\n                                                <property name=\"visible\">True</property>\n                                                <property name=\"can_focus\">False</property>\n                                                <property name=\"stock\">gtk-stop</property>\n                                              </object>\n                                            </child>\n                                          </object>\n                                        </child>\n                                      </object>\n                                      <packing>\n                                        <property name=\"expand\">False</property>\n                                        <property name=\"homogeneous\">False</property>\n                                      </packing>\n                                    </child>\n                                  </object>\n                                  <packing>\n                                    <property name=\"expand\">False</property>\n                                    <property name=\"fill\">True</property>\n                                    <property name=\"position\">1</property>\n                                  </packing>\n                                </child>\n                              </object>\n                              <packing>\n                                <property name=\"expand\">False</property>\n                                <property name=\"fill\">False</property>\n                                <property name=\"position\">0</property>\n                              </packing>\n                            </child>\n                            <child>\n                              <object class=\"GtkNotebook\" id=\"scriptNotebook\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">True</property>\n                                <property name=\"scrollable\">True</property>\n                              </object>\n                              <packing>\n                                <property name=\"expand\">True</property>\n                                <property name=\"fill\">True</property>\n                                <property name=\"position\">1</property>\n                              </packing>\n                            </child>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">True</property>\n                            <property name=\"fill\">True</property>\n                            <property name=\"position\">1</property>\n                          </packing>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"resize\">False</property>\n                        <property name=\"shrink\">True</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkPaned\" id=\"vpaned1\">\n                        <property name=\"width_request\">250</property>\n                        <property name=\"height_request\">500</property>\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">True</property>\n                        <property name=\"orientation\">vertical</property>\n                        <property name=\"position\">380</property>\n                        <child>\n                          <object class=\"GtkNotebook\" id=\"sequentsNotebook\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">True</property>\n                            <property name=\"scrollable\">True</property>\n                          </object>\n                          <packing>\n                            <property name=\"resize\">False</property>\n                            <property name=\"shrink\">True</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkBox\" id=\"hbox9\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <child>\n                              <object class=\"GtkScrolledWindow\" id=\"logScrolledWin\">\n                                <property name=\"visible\">True</property>\n                                <property name=\"can_focus\">True</property>\n                                <property name=\"hscrollbar_policy\">never</property>\n                                <property name=\"shadow_type\">in</property>\n                                <child>\n                                  <object class=\"GtkTextView\" id=\"logTextView\">\n                                    <property name=\"visible\">True</property>\n                                    <property name=\"can_focus\">True</property>\n                                    <property name=\"editable\">False</property>\n                                    <property name=\"wrap_mode\">char</property>\n                                    <property name=\"cursor_visible\">False</property>\n                                  </object>\n                                </child>\n                              </object>\n                              <packing>\n                                <property name=\"expand\">True</property>\n                                <property name=\"fill\">True</property>\n                                <property name=\"position\">0</property>\n                              </packing>\n                            </child>\n                          </object>\n                          <packing>\n                            <property name=\"resize\">True</property>\n                            <property name=\"shrink\">True</property>\n                          </packing>\n                        </child>\n                      </object>\n                      <packing>\n                        <property name=\"resize\">True</property>\n                        <property name=\"shrink\">True</property>\n                      </packing>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">True</property>\n                    <property name=\"fill\">True</property>\n                    <property name=\"position\">0</property>\n                  </packing>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkBox\" id=\"hbox10\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <child>\n                  <object class=\"GtkStatusbar\" id=\"StatusBar\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">True</property>\n                    <property name=\"fill\">True</property>\n                    <property name=\"position\">0</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkNotebook\" id=\"HintNotebook\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"show_tabs\">False</property>\n                    <child>\n                      <object class=\"GtkImage\" id=\"HintLowImage\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"stock\">gtk-missing-image</property>\n                      </object>\n                    </child>\n                    <child type=\"tab\">\n                      <object class=\"GtkLabel\" id=\"label14\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"label\" translatable=\"yes\">label14</property>\n                      </object>\n                      <packing>\n                        <property name=\"tab_fill\">False</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkImage\" id=\"HintMediumImage\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"stock\">gtk-missing-image</property>\n                      </object>\n                      <packing>\n                        <property name=\"position\">1</property>\n                      </packing>\n                    </child>\n                    <child type=\"tab\">\n                      <object class=\"GtkLabel\" id=\"label15\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"label\" translatable=\"yes\">label15</property>\n                      </object>\n                      <packing>\n                        <property name=\"position\">1</property>\n                        <property name=\"tab_fill\">False</property>\n                      </packing>\n                    </child>\n                    <child>\n                      <object class=\"GtkImage\" id=\"HintHighImage\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"stock\">gtk-missing-image</property>\n                      </object>\n                      <packing>\n                        <property name=\"position\">2</property>\n                      </packing>\n                    </child>\n                    <child type=\"tab\">\n                      <object class=\"GtkLabel\" id=\"label16\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"label\" translatable=\"yes\">label16</property>\n                      </object>\n                      <packing>\n                        <property name=\"position\">2</property>\n                        <property name=\"tab_fill\">False</property>\n                      </packing>\n                    </child>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">False</property>\n                    <property name=\"fill\">True</property>\n                    <property name=\"position\">1</property>\n                  </packing>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">2</property>\n              </packing>\n            </child>\n          </object>\n        </child>\n      </object>\n    </child>\n  </object>\n  <object class=\"GtkDialog\" id=\"UriChoiceDialog\">\n    <property name=\"height_request\">280</property>\n    <property name=\"can_focus\">False</property>\n    <property name=\"title\" translatable=\"yes\">Uri choice</property>\n    <property name=\"modal\">True</property>\n    <property name=\"window_position\">center</property>\n    <property name=\"type_hint\">dialog</property>\n    <child internal-child=\"vbox\">\n      <object class=\"GtkBox\" id=\"dialog-vbox3\">\n        <property name=\"visible\">True</property>\n        <property name=\"can_focus\">False</property>\n        <property name=\"orientation\">vertical</property>\n        <property name=\"spacing\">4</property>\n        <child internal-child=\"action_area\">\n          <object class=\"GtkButtonBox\" id=\"dialog-action_area3\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"layout_style\">end</property>\n            <child>\n              <object class=\"GtkButton\" id=\"UriChoiceAbortButton\">\n                <property name=\"label\">gtk-cancel</property>\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"can_default\">True</property>\n                <property name=\"receives_default\">False</property>\n                <property name=\"use_stock\">True</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"UriChoiceSelectedButton\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"can_default\">True</property>\n                <property name=\"receives_default\">False</property>\n                <child>\n                  <object class=\"GtkAlignment\" id=\"alignment2\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"xscale\">0</property>\n                    <property name=\"yscale\">0</property>\n                    <child>\n                      <object class=\"GtkBox\" id=\"hbox3\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"spacing\">2</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image19\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-index</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">0</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkLabel\" id=\"label3\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">Try _Selected</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">1</property>\n                          </packing>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"UriChoiceConstantsButton\">\n                <property name=\"label\" translatable=\"yes\">Try Constants</property>\n                <property name=\"visible\">True</property>\n                <property name=\"sensitive\">False</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"can_default\">True</property>\n                <property name=\"receives_default\">False</property>\n                <property name=\"use_underline\">True</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">2</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"copyButton\">\n                <property name=\"label\">gtk-copy</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"can_default\">True</property>\n                <property name=\"receives_default\">False</property>\n                <property name=\"use_stock\">True</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">3</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"uriChoiceAutoButton\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"can_default\">True</property>\n                <property name=\"receives_default\">False</property>\n                <child>\n                  <object class=\"GtkAlignment\" id=\"alignment5\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"xscale\">0</property>\n                    <property name=\"yscale\">0</property>\n                    <child>\n                      <object class=\"GtkBox\" id=\"hbox16\">\n                        <property name=\"visible\">True</property>\n                        <property name=\"can_focus\">False</property>\n                        <property name=\"spacing\">2</property>\n                        <child>\n                          <object class=\"GtkImage\" id=\"image302\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"stock\">gtk-ok</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">0</property>\n                          </packing>\n                        </child>\n                        <child>\n                          <object class=\"GtkLabel\" id=\"okLabel\">\n                            <property name=\"visible\">True</property>\n                            <property name=\"can_focus\">False</property>\n                            <property name=\"label\" translatable=\"yes\">bla bla bla</property>\n                            <property name=\"use_underline\">True</property>\n                          </object>\n                          <packing>\n                            <property name=\"expand\">False</property>\n                            <property name=\"fill\">False</property>\n                            <property name=\"position\">1</property>\n                          </packing>\n                        </child>\n                      </object>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">4</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkButton\" id=\"uriChoiceForwardButton\">\n                <property name=\"label\">gtk-go-forward</property>\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"can_default\">True</property>\n                <property name=\"receives_default\">False</property>\n                <property name=\"use_stock\">True</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">5</property>\n              </packing>\n            </child>\n          </object>\n          <packing>\n            <property name=\"expand\">False</property>\n            <property name=\"fill\">False</property>\n            <property name=\"pack_type\">end</property>\n            <property name=\"position\">0</property>\n          </packing>\n        </child>\n        <child>\n          <object class=\"GtkBox\" id=\"vbox2\">\n            <property name=\"visible\">True</property>\n            <property name=\"can_focus\">False</property>\n            <property name=\"orientation\">vertical</property>\n            <property name=\"spacing\">3</property>\n            <child>\n              <object class=\"GtkLabel\" id=\"UriChoiceLabel\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"label\" translatable=\"yes\">some informative message here ...</property>\n              </object>\n              <packing>\n                <property name=\"expand\">False</property>\n                <property name=\"fill\">False</property>\n                <property name=\"position\">0</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkScrolledWindow\" id=\"scrolledwindow1\">\n                <property name=\"width_request\">400</property>\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">True</property>\n                <property name=\"vexpand\">True</property>\n                <child>\n                  <object class=\"GtkTreeView\" id=\"UriChoiceTreeView\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                    <property name=\"headers_visible\">False</property>\n                    <child internal-child=\"selection\">\n                      <object class=\"GtkTreeSelection\"/>\n                    </child>\n                  </object>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">1</property>\n              </packing>\n            </child>\n            <child>\n              <object class=\"GtkBox\" id=\"uriEntryHBox\">\n                <property name=\"visible\">True</property>\n                <property name=\"can_focus\">False</property>\n                <property name=\"vexpand\">True</property>\n                <child>\n                  <object class=\"GtkLabel\" id=\"label2\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">False</property>\n                    <property name=\"label\" translatable=\"yes\">URI: </property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">False</property>\n                    <property name=\"fill\">False</property>\n                    <property name=\"position\">0</property>\n                  </packing>\n                </child>\n                <child>\n                  <object class=\"GtkEntry\" id=\"entry1\">\n                    <property name=\"visible\">True</property>\n                    <property name=\"can_focus\">True</property>\n                  </object>\n                  <packing>\n                    <property name=\"expand\">True</property>\n                    <property name=\"fill\">True</property>\n                    <property name=\"position\">1</property>\n                  </packing>\n                </child>\n              </object>\n              <packing>\n                <property name=\"expand\">True</property>\n                <property name=\"fill\">True</property>\n                <property name=\"position\">2</property>\n              </packing>\n            </child>\n          </object>\n          <packing>\n            <property name=\"expand\">False</property>\n            <property name=\"fill\">True</property>\n            <property name=\"position\">2</property>\n          </packing>\n        </child>\n      </object>\n    </child>\n    <action-widgets>\n      <action-widget response=\"-6\">UriChoiceAbortButton</action-widget>\n    </action-widgets>\n  </object>\n</interface>\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
Unnamed repository; edit this file 'description' to name the repository.