--- /dev/null
+*.a
+*.annot
+autom4te.cache
+buildTimeConf.ml
+cicbrowser
+cicbrowser.opt
+*.cma
+*.cmi
+*.cmo
+*.cmx
+*.cmxa
+config.log
+config.status
+configure
+.depend
+Makefile
+matita
+.matita
+matitac
+matitac.opt
+matitaGeneratedGui.ml
+matitaGeneratedGui.mli
+matita.glade.bak
+matita.gladep
+matita.gladep.bak
+matita.opt
+matita.opt
+*.o
+*.swp
--- /dev/null
+matitac.cmo: matitaTypes.cmo matitaLog.cmi matitaEngine.cmi matitaDb.cmi \
+ buildTimeConf.cmo
+matitac.cmx: matitaTypes.cmx matitaLog.cmx matitaEngine.cmx matitaDb.cmx \
+ buildTimeConf.cmx
+matitaDb.cmo: matitaDb.cmi
+matitaDb.cmx: matitaDb.cmi
+matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi
+matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi
+matitaEngine.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \
+ matitaDisambiguator.cmi matitaDb.cmi matitaEngine.cmi
+matitaEngine.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \
+ matitaDisambiguator.cmx matitaDb.cmx matitaEngine.cmi
+matitaGeneratedGui.cmo: matitaGeneratedGui.cmi
+matitaGeneratedGui.cmx: matitaGeneratedGui.cmi
+matitaGtkMisc.cmo: matitaTypes.cmo matitaGeneratedGui.cmi matitaGtkMisc.cmi
+matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi
+matitaGui.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi matitaLog.cmi \
+ matitaGtkMisc.cmi matitaGeneratedGui.cmi buildTimeConf.cmo matitaGui.cmi
+matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx matitaLog.cmx \
+ matitaGtkMisc.cmx matitaGeneratedGui.cmx buildTimeConf.cmx matitaGui.cmi
+matitaLog.cmo: matitaLog.cmi
+matitaLog.cmx: matitaLog.cmi
+matitaMathView.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \
+ matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo matitaMathView.cmi
+matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
+ matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx matitaMathView.cmi
+matitaMisc.cmo: matitaTypes.cmo buildTimeConf.cmo matitaMisc.cmi
+matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi
+matita.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \
+ matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \
+ matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo
+matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
+ matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \
+ matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx
+matitaScript.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \
+ matitaEngine.cmi matitaScript.cmi
+matitaScript.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \
+ matitaEngine.cmx matitaScript.cmi
+matitaSync.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
+ matitaSync.cmi
+matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
+ matitaSync.cmi
+matitaTypes.cmo: matitaLog.cmi
+matitaTypes.cmx: matitaLog.cmx
+matitaDisambiguator.cmi: matitaTypes.cmo
+matitaEngine.cmi: matitaTypes.cmo
+matitaGtkMisc.cmi: matitaGeneratedGui.cmi
+matitaGui.cmi: matitaLog.cmi matitaGeneratedGui.cmi matitaDisambiguator.cmi
+matitaMisc.cmi: matitaTypes.cmo
+matitaScript.cmi: matitaTypes.cmo
+matitaSync.cmi: matitaTypes.cmo
--- /dev/null
+
+OCAMLFIND = @OCAMLFIND@
+CAMLP4O = @CAMLP4O@
+LABLGLADECC = @LABLGLADECC@
+REQUIRES = @FINDLIB_REQUIRES@
+CREQUIRES = @FINDLIB_CREQUIRES@
+HAVE_OCAMLOPT = @HAVE_OCAMLOPT@
+
+OCAML_FLAGS = -pp $(CAMLP4O)
+PKGS = -package "$(REQUIRES)"
+CPKGS = -package "$(CREQUIRES)"
+OCAML_THREADS_FLAGS = -thread
+OCAML_DEBUG_FLAGS = -g
+OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS)
+OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS)
+OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS)
+OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS)
+# objects for matita (GTK GUI)
+CMOS = \
+ buildTimeConf.cmo \
+ matitaLog.cmo \
+ matitaTypes.cmo \
+ matitaMisc.cmo \
+ matitaDb.cmo \
+ matitaSync.cmo \
+ matitaDisambiguator.cmo \
+ matitaEngine.cmo \
+ matitaScript.cmo \
+ matitaGeneratedGui.cmo \
+ matitaGtkMisc.cmo \
+ matitaGui.cmo \
+ matitaMathView.cmo
+# objects for matitac (batch compiler)
+CCMOS = \
+ buildTimeConf.cmo \
+ matitaLog.cmo \
+ matitaTypes.cmo \
+ matitaMisc.cmo \
+ matitaDb.cmo \
+ matitaSync.cmo \
+ matitaDisambiguator.cmo \
+ matitaEngine.cmo
+
+LIB_DEPS = $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES))
+
+all: matita matitac cicbrowser
+
+ifeq ($(HAVE_OCAMLOPT),yes)
+CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
+CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
+LIBX_DEPS = $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES))
+opt: matita.opt matitac.opt cicbrowser.opt
+else
+opt:
+ @echo "Native code compilation is disabled"
+endif
+
+matita: $(LIB_DEPS) $(CMOS) matita.ml
+ $(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml
+matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml
+ $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml
+
+matitac: $(LIB_DEPS) $(CCMOS) matitac.ml
+ $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) matitac.ml
+matitac.opt: $(LIBX_DEPS) $(CMXS) matitac.ml
+ $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml
+
+cicbrowser: matita
+ @test -f $@ || ln -s $< $@
+cicbrowser.opt: matita.opt
+ @test -f $@ || ln -s $< $@
+
+matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade
+ $(LABLGLADECC) -embed $< > matitaGeneratedGui.ml
+ $(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli
+
+%.cmi: %.mli
+ $(OCAMLC) $(PKGS) -c $<
+%.cmo %.cmi: %.ml
+ $(OCAMLC) $(PKGS) -c $<
+%.cmx: %.ml
+ $(OCAMLOPT) $(PKGS) -c $<
+%.annot: %.ml
+ $(OCAMLC) -dtypes $(PKGS) -c $<
+
+clean:
+ rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \
+ matita matita.opt matitac matitac.opt \
+ cicbrowser cicbrowser.opt
+distclean: clean
+ rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
+ rm -f config.log config.status Makefile buildTimeConf.ml
+ rm -f matita.glade.bak matita.gladep.bak
+ rm -rf autom4te.cache/
+
+#.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli
+.depend:
+ $(OCAMLDEP) *.ml *.mli > .depend
+
+include .depend
+
+.PHONY: all opt clean distclean depend
+
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+let debug = @DEBUG@;;
+let version = "0.0.1";;
+let undo_history_size = 10;;
+let console_history_size = 100;;
+let browser_history_size = 100;;
+let gtkrc = "@MATITA_GTKRC@";;
+let base_uri = "cic:/matita";;
+let phrase_sep = ".";;
+let blank_uri = "about:blank";;
+let current_proof_uri = "about:current_proof";;
+
--- /dev/null
+AC_INIT(matitaTypes.ml)
+
+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, lablgladecc2, yes, no)
+if test $HAVE_LABLGLADECC = "yes"; then
+ LABLGLADECC="lablgladecc2"
+else
+ AC_MSG_ERROR(could not find lablgladecc2)
+fi
+AC_CHECK_PROG(HAVE_CAMLP4O, camlp4o, yes, no)
+if test $HAVE_CAMLP4O = "yes"; then
+ CAMLP4O="camlp4o"
+else
+ AC_MSG_ERROR(could not find camlp4o)
+fi
+
+FINDLIB_CREQUIRES="\
+pcre \
+mysql \
+unix \
+helm-cic_omdoc \
+helm-cic_transformations \
+helm-registry \
+helm-tactics \
+helm-xml \
+helm-cic_textual_parser2 \
+"
+FINDLIB_REQUIRES="\
+$FINDLIB_CREQUIRES \
+lablgtk2.glade \
+lablgtkmathview \
+helm-xmldiff \
+"
+for r in $FINDLIB_REQUIRES
+do
+ AC_MSG_CHECKING(for $r ocaml library)
+ if $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_ARG_ENABLE(debug,
+ [ --enable-debug Turn on debugging],
+ [case "${enableval}" in
+ yes) DEBUG=true ;;
+ no) DEBUG=false ;;
+ *) AC_MSG_ERROR(bad value ${enableval} for --enable-debug) ;;
+ esac],
+ [DEBUG=true])
+if test "$DEBUG" = "true"; then
+ echo "debugging enabled"
+fi
+
+MATITA_GTKRC="matita.gtkrc"
+
+AC_SUBST(CAMLP4O)
+AC_SUBST(DEBUG)
+AC_SUBST(TRANSFORMER_MODULE)
+AC_SUBST(FINDLIB_REQUIRES)
+AC_SUBST(FINDLIB_CREQUIRES)
+AC_SUBST(HAVE_OCAMLOPT)
+AC_SUBST(LABLGLADECC)
+AC_SUBST(OCAMLFIND)
+AC_SUBST(MATITA_GTKRC)
+
+AC_OUTPUT([
+ buildTimeConf.ml
+ Makefile
+])
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="matita">
+ <key name="auto_disambiguation">true</key>
+ <key name="environment_trust">true</key>
+ <key name="baseuri">cic:/matita/</key>
+ <key name="basedir">.matita/xml</key>
+ <key name="owner">gares</key>
+ </section>
+ <section name="db">
+<!-- <key name="host">localhost</key> -->
+ <key name="host">mowgli.cs.unibo.it</key>
+ <key name="user">helm</key>
+ <key name="database">matita</key>
+ </section>
+ <section name="getter">
+ <key name="prefetch">true</key>
+ <key name="servers">
+ file:///projects/helm/library/coq_contribs
+ </key>
+ <key name="cache_dir">.matita/getter/cache</key>
+ <key name="maps_dir">.matita/getter/maps</key>
+ <key name="dtd_dir">/projects/helm/xml/dtd</key>
+<!-- <key name="loglevel">180</key> -->
+ </section>
+</helm_registry>
--- /dev/null
+<?xml version="1.0" standalone="no"?> <!--*- mode: xml -*-->
+<!DOCTYPE glade-interface SYSTEM "http://glade.gnome.org/glade-2.0.dtd">
+
+<glade-interface>
+
+<widget class="GtkDialog" id="AboutWin">
+ <property name="title" translatable="yes">Matita: about</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_CENTER</property>
+ <property name="modal">True</property>
+ <property name="resizable">False</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="dialog-vbox2">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="dialog-action_area2">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="AboutDismissButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-ok</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-5</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="AboutLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes"><b>Matita @VERSION@</b>
+
+<tt>http://helm.cs.unibo.it</tt>
+
+Copyright (C) 2005,
+<i>the HELM team</i></property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">True</property>
+ <property name="justify">GTK_JUSTIFY_CENTER</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">5</property>
+ <property name="ypad">5</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkWindow" id="BrowserWin">
+ <property name="width_request">500</property>
+ <property name="height_request">500</property>
+ <property name="visible">True</property>
+ <property name="title" translatable="yes">Cic browser</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+
+ <child>
+ <widget class="GtkEventBox" id="BrowserWinEventBox">
+ <property name="visible">True</property>
+ <property name="visible_window">True</property>
+ <property name="above_child">False</property>
+
+ <child>
+ <widget class="GtkVBox" id="BrowserVBox">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkHandleBox" id="handlebox1">
+ <property name="visible">True</property>
+ <property name="shadow_type">GTK_SHADOW_OUT</property>
+ <property name="handle_position">GTK_POS_LEFT</property>
+ <property name="snap_edge">GTK_POS_TOP</property>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar14">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem30">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="BrowserNewButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">new browser win</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NONE</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image191">
+ <property name="visible">True</property>
+ <property name="stock">gtk-new</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem31">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="BrowserBackButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">history back</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NONE</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkAlignment" id="alignment3">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xscale">0</property>
+ <property name="yscale">0</property>
+ <property name="top_padding">0</property>
+ <property name="bottom_padding">0</property>
+ <property name="left_padding">0</property>
+ <property name="right_padding">0</property>
+
+ <child>
+ <widget class="GtkHBox" id="hbox6">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
+
+ <child>
+ <widget class="GtkImage" id="image188">
+ <property name="visible">True</property>
+ <property name="stock">gtk-go-back</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label10">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes"></property>
+ <property name="use_underline">True</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem32">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="BrowserForwardButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">history forward</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NONE</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image189">
+ <property name="visible">True</property>
+ <property name="stock">gtk-go-forward</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem33">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="BrowserRefreshButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">refresh</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NONE</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image229">
+ <property name="visible">True</property>
+ <property name="stock">gtk-refresh</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem34">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="BrowserHomeButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">home</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NONE</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image190">
+ <property name="visible">True</property>
+ <property name="stock">gtk-home</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem35">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkImage" id="image187">
+ <property name="visible">True</property>
+ <property name="stock">gtk-jump-to</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem36">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkEntry" id="BrowserUri">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">cic uri</property>
+ <property name="can_focus">True</property>
+ <property name="editable">True</property>
+ <property name="visibility">True</property>
+ <property name="max_length">0</property>
+ <property name="text" translatable="yes"></property>
+ <property name="has_frame">True</property>
+ <property name="invisible_char">*</property>
+ <property name="activates_default">False</property>
+ <property name="width_chars">34</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkFrame" id="frame1">
+ <property name="visible">True</property>
+ <property name="label_xalign">0</property>
+ <property name="label_yalign">0</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="ScrolledBrowser">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_NONE</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <placeholder/>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkDialog" id="ConfirmationDialog">
+ <property name="title" translatable="yes">DUMMY</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_CENTER</property>
+ <property name="modal">True</property>
+ <property name="resizable">False</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="dialog-vbox1">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="dialog-action_area1">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="ConfirmationDialogCancelButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-cancel</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-6</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="ConfirmationDialogOkButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-ok</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-5</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="ConfirmationDialogLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">DUMMY</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_CENTER</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkDialog" id="EmptyDialog">
+ <property name="visible">True</property>
+ <property name="title" translatable="yes">DUMMY</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="EmptyDialogVBox">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="dialog-action_area5">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="EmptyDialogCancelButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-cancel</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-6</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="EmptyDialogOkButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-ok</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-5</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="EmptyDialogLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">DUMMY</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <placeholder/>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkFileSelection" id="FileSelectionWin">
+ <property name="border_width">10</property>
+ <property name="title" translatable="yes">Select File</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_CENTER</property>
+ <property name="modal">True</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+ <property name="show_fileops">True</property>
+
+ <child internal-child="cancel_button">
+ <widget class="GtkButton" id="fileSelCancelButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+
+ <child internal-child="ok_button">
+ <widget class="GtkButton" id="fileSelOkButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkDialog" id="InterpChoiceDialog">
+ <property name="height_request">200</property>
+ <property name="title" translatable="yes">Interpretation choice</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">True</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="dialog-vbox4">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="dialog-action_area4">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="InterpChoiceHelpButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-help</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-11</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="InterpChoiceCancelButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-cancel</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-6</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="InterpChoiceOkButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-ok</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-5</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkVBox" id="vbox3">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkLabel" id="InterpChoiceDialogLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">some informative message here ...</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="scrolledwindow4">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTreeView" id="InterpChoiceTreeView">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="headers_visible">False</property>
+ <property name="rules_hint">False</property>
+ <property name="reorderable">False</property>
+ <property name="enable_search">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkWindow" id="MainWin">
+ <property name="title" translatable="yes">Matita</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="default_width">800</property>
+ <property name="default_height">600</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+
+ <child>
+ <widget class="GtkEventBox" id="MainWinEventBox">
+ <property name="visible">True</property>
+ <property name="visible_window">True</property>
+ <property name="above_child">False</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox8">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkHandleBox" id="menuBarHandleBox">
+ <property name="visible">True</property>
+ <property name="shadow_type">GTK_SHADOW_OUT</property>
+ <property name="handle_position">GTK_POS_LEFT</property>
+ <property name="snap_edge">GTK_POS_TOP</property>
+
+ <child>
+ <widget class="GtkMenuBar" id="menubar1">
+ <property name="visible">True</property>
+
+ <child>
+ <widget class="GtkMenuItem" id="fileMenu">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_File</property>
+ <property name="use_underline">True</property>
+
+ <child>
+ <widget class="GtkMenu" id="fileMenu_menu">
+
+ <child>
+ <widget class="GtkImageMenuItem" id="newMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_New</property>
+ <property name="use_underline">True</property>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image290">
+ <property name="visible">True</property>
+ <property name="stock">gtk-new</property>
+ <property name="icon_size">1</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkImageMenuItem" id="openMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Open...</property>
+ <property name="use_underline">True</property>
+ <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image291">
+ <property name="visible">True</property>
+ <property name="stock">gtk-open</property>
+ <property name="icon_size">1</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkImageMenuItem" id="saveMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Save</property>
+ <property name="use_underline">True</property>
+ <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image292">
+ <property name="visible">True</property>
+ <property name="stock">gtk-save</property>
+ <property name="icon_size">1</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkImageMenuItem" id="saveAsMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Save _As ...</property>
+ <property name="use_underline">True</property>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image293">
+ <property name="visible">True</property>
+ <property name="stock">gtk-save-as</property>
+ <property name="icon_size">1</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkSeparatorMenuItem" id="separatormenuitem3">
+ <property name="visible">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkImageMenuItem" id="quitMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Quit</property>
+ <property name="use_underline">True</property>
+ <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image294">
+ <property name="visible">True</property>
+ <property name="stock">gtk-quit</property>
+ <property name="icon_size">1</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="editMenu">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Edit</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="viewMenu">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_View</property>
+ <property name="use_underline">True</property>
+
+ <child>
+ <widget class="GtkMenu" id="viewMenu_menu">
+
+ <child>
+ <widget class="GtkMenuItem" id="newCicBrowserMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">New Cic Browser</property>
+ <property name="use_underline">True</property>
+ <accelerator key="F3" modifiers="0" signal="activate"/>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="debugMenu">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Debug</property>
+ <property name="use_underline">True</property>
+
+ <child>
+ <widget class="GtkMenu" id="debugMenu_menu">
+
+ <child>
+ <widget class="GtkSeparatorMenuItem" id="separatormenuitem5">
+ <property name="visible">True</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="helpMenu">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Help</property>
+ <property name="use_underline">True</property>
+
+ <child>
+ <widget class="GtkMenu" id="helpMenu_menu">
+
+ <child>
+ <widget class="GtkMenuItem" id="aboutMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">About...</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHBox" id="hbox9">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkHandleBox" id="handlebox7">
+ <property name="visible">True</property>
+ <property name="shadow_type">GTK_SHADOW_OUT</property>
+ <property name="handle_position">GTK_POS_TOP</property>
+ <property name="snap_edge">GTK_POS_TOP</property>
+
+ <child>
+ <widget class="GtkVBox" id="ToolBarVBox">
+ <property name="width_request">102</property>
+ <property name="visible">True</property>
+ <property name="homogeneous">True</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox10">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar11">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem4">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="introsButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Intros</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">intros</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem5">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="applyButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Apply</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">apply</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar12">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem6">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="exactButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Exact</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">exact</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar3">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem7">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="elimButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Elim</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">elim</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem8">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="elimTypeButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">ElimType</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">elimTy</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar4">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem9">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="splitButton">
+ <property name="width_request">25</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Split</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">∧</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem10">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="leftButton">
+ <property name="width_request">25</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Left</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">L</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem11">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="rightButton">
+ <property name="width_request">25</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Right</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">R</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem12">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="existsButton">
+ <property name="width_request">25</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Exists</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">∃</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkVBox" id="vbox12">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar5">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem14">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="reflexivityButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Reflexivity</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">refl</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem15">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="symmetryButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Symmetry</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">sym</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar9">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem16">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="transitivityButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Transitivity</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">trans</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkVBox" id="vbox11">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar8">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem22">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="simplifyButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Simplify</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">simpl</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem23">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="reduceButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Reduce</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">red</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar10">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem24">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="whdButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Whd</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">whd</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar6">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem17">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="assumptionButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Assumption</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">asum</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem18">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="autoButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Auto</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">auto</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar7">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem20">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="cutButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Cut</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">cut</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem21">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="replaceButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Replace</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">repl</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHPaned" id="hpaned1">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox9">
+ <property name="width_request">400</property>
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar13">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem25">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="scriptTopButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">restart</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NONE</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image253">
+ <property name="visible">True</property>
+ <property name="stock">gtk-goto-top</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem26">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="scriptRetractButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">go back 1 phrase</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NONE</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image254">
+ <property name="visible">True</property>
+ <property name="stock">gtk-go-up</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem27">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="scriptJumpButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">execute until point</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NONE</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image255">
+ <property name="visible">True</property>
+ <property name="stock">gtk-jump-to</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem28">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="scriptAdvanceButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">go forward 1 phrase</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NONE</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image256">
+ <property name="visible">True</property>
+ <property name="stock">gtk-go-down</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem29">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="scriptBottomButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">execute all</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NONE</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image257">
+ <property name="visible">True</property>
+ <property name="stock">gtk-goto-bottom</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkNotebook" id="scriptNotebokk">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="show_tabs">True</property>
+ <property name="show_border">True</property>
+ <property name="tab_pos">GTK_POS_BOTTOM</property>
+ <property name="scrollable">False</property>
+ <property name="enable_popup">False</property>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="scrolledwindow7">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_NONE</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTextView" id="scriptTextView">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="editable">True</property>
+ <property name="overwrite">False</property>
+ <property name="accepts_tab">True</property>
+ <property name="justification">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap_mode">GTK_WRAP_NONE</property>
+ <property name="cursor_visible">True</property>
+ <property name="pixels_above_lines">0</property>
+ <property name="pixels_below_lines">0</property>
+ <property name="pixels_inside_wrap">0</property>
+ <property name="left_margin">0</property>
+ <property name="right_margin">0</property>
+ <property name="indent">0</property>
+ <property name="text" translatable="yes"></property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="tab_expand">False</property>
+ <property name="tab_fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label12">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">script</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="type">tab</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="scrolledwindow8">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_NONE</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTreeView" id="scriptTreeView">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="headers_visible">False</property>
+ <property name="rules_hint">False</property>
+ <property name="reorderable">False</property>
+ <property name="enable_search">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="tab_expand">False</property>
+ <property name="tab_fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label13">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">outline</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="type">tab</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="shrink">True</property>
+ <property name="resize">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkVPaned" id="vpaned1">
+ <property name="width_request">450</property>
+ <property name="height_request">500</property>
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="position">450</property>
+
+ <child>
+ <widget class="GtkNotebook" id="sequentsNotebook">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="show_tabs">True</property>
+ <property name="show_border">True</property>
+ <property name="tab_pos">GTK_POS_TOP</property>
+ <property name="scrollable">False</property>
+ <property name="enable_popup">False</property>
+ </widget>
+ <packing>
+ <property name="shrink">True</property>
+ <property name="resize">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHBox" id="hbox9">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="logScrolledWin">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
+ <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTextView" id="logTextView">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="editable">False</property>
+ <property name="overwrite">False</property>
+ <property name="accepts_tab">True</property>
+ <property name="justification">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap_mode">GTK_WRAP_CHAR</property>
+ <property name="cursor_visible">False</property>
+ <property name="pixels_above_lines">0</property>
+ <property name="pixels_below_lines">0</property>
+ <property name="pixels_inside_wrap">0</property>
+ <property name="left_margin">0</property>
+ <property name="right_margin">0</property>
+ <property name="indent">0</property>
+ <property name="text" translatable="yes"></property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="shrink">True</property>
+ <property name="resize">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="shrink">False</property>
+ <property name="resize">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHBox" id="hbox10">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkStatusbar" id="StatusBar">
+ <property name="visible">True</property>
+ <property name="has_resize_grip">True</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkNotebook" id="HintNotebook">
+ <property name="visible">True</property>
+ <property name="show_tabs">False</property>
+ <property name="show_border">True</property>
+ <property name="tab_pos">GTK_POS_TOP</property>
+ <property name="scrollable">False</property>
+ <property name="enable_popup">False</property>
+
+ <child>
+ <widget class="GtkImage" id="HintLowImage">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="tab_expand">False</property>
+ <property name="tab_fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label14">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">label14</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="type">tab</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkImage" id="HintMediumImage">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="tab_expand">False</property>
+ <property name="tab_fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label15">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">label15</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="type">tab</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkImage" id="HintHighImage">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="tab_expand">False</property>
+ <property name="tab_fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label16">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">label16</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="type">tab</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkDialog" id="TextDialog">
+ <property name="title" translatable="yes">DUMMY</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="vbox5">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="hbuttonbox1">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="TextDialogCancelButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-cancel</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-6</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="TextDialogOkButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-ok</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-5</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="TextDialogLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">DUMMY</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="scrolledwindow2">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTextView" id="TextDialogTextView">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="editable">True</property>
+ <property name="overwrite">False</property>
+ <property name="accepts_tab">True</property>
+ <property name="justification">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap_mode">GTK_WRAP_NONE</property>
+ <property name="cursor_visible">True</property>
+ <property name="pixels_above_lines">0</property>
+ <property name="pixels_below_lines">0</property>
+ <property name="pixels_inside_wrap">0</property>
+ <property name="left_margin">0</property>
+ <property name="right_margin">0</property>
+ <property name="indent">0</property>
+ <property name="text" translatable="yes"></property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkDialog" id="UriChoiceDialog">
+ <property name="height_request">280</property>
+ <property name="title" translatable="yes">Uri choice</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_CENTER</property>
+ <property name="modal">True</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="dialog-vbox3">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="dialog-action_area3">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="UriChoiceAbortButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-cancel</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-6</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="UriChoiceSelectedButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">0</property>
+
+ <child>
+ <widget class="GtkAlignment" id="alignment2">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xscale">0</property>
+ <property name="yscale">0</property>
+ <property name="top_padding">0</property>
+ <property name="bottom_padding">0</property>
+ <property name="left_padding">0</property>
+ <property name="right_padding">0</property>
+
+ <child>
+ <widget class="GtkHBox" id="hbox3">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
+
+ <child>
+ <widget class="GtkImage" id="image19">
+ <property name="visible">True</property>
+ <property name="stock">gtk-index</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label3">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Try _Selected</property>
+ <property name="use_underline">True</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="UriChoiceConstantsButton">
+ <property name="visible">True</property>
+ <property name="sensitive">False</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">Try Constants</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">0</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="UriChoiceAutoButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">0</property>
+
+ <child>
+ <widget class="GtkAlignment" id="alignment1">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xscale">0</property>
+ <property name="yscale">0</property>
+ <property name="top_padding">0</property>
+ <property name="bottom_padding">0</property>
+ <property name="left_padding">0</property>
+ <property name="right_padding">0</property>
+
+ <child>
+ <widget class="GtkHBox" id="hbox1">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
+
+ <child>
+ <widget class="GtkImage" id="image18">
+ <property name="visible">True</property>
+ <property name="stock">gtk-ok</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label1">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Auto</property>
+ <property name="use_underline">True</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkVBox" id="vbox2">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkLabel" id="UriChoiceLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">some informative message here ...</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="scrolledwindow1">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="shadow_type">GTK_SHADOW_NONE</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTreeView" id="UriChoiceTreeView">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="headers_visible">False</property>
+ <property name="rules_hint">False</property>
+ <property name="reorderable">False</property>
+ <property name="enable_search">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHBox" id="hbox2">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkLabel" id="label2">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">URI: </property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkEntry" id="entry1">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="editable">True</property>
+ <property name="visibility">True</property>
+ <property name="max_length">0</property>
+ <property name="text" translatable="yes"></property>
+ <property name="has_frame">True</property>
+ <property name="invisible_char">*</property>
+ <property name="activates_default">False</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+</glade-interface>
--- /dev/null
+# Based on /usr/share/themes/Emacs/gtk-2.0-key/,
+# modified by Zack for matita
+
+#
+# A keybinding set implementing emacs-like keybindings
+#
+
+#
+# Bindings for GtkTextView and GtkEntry
+#
+binding "gtk-emacs-text-entry"
+{
+ bind "<ctrl>b" { "move-cursor" (logical-positions, -1, 0) }
+ bind "<shift><ctrl>b" { "move-cursor" (logical-positions, -1, 1) }
+ bind "<ctrl>f" { "move-cursor" (logical-positions, 1, 0) }
+ bind "<shift><ctrl>f" { "move-cursor" (logical-positions, 1, 1) }
+
+ bind "<alt>b" { "move-cursor" (words, -1, 0) }
+ bind "<shift><alt>b" { "move-cursor" (words, -1, 1) }
+ bind "<alt>f" { "move-cursor" (words, 1, 0) }
+ bind "<shift><alt>f" { "move-cursor" (words, 1, 1) }
+
+ bind "<ctrl>a" { "move-cursor" (paragraph-ends, -1, 0) }
+ bind "<shift><ctrl>a" { "move-cursor" (paragraph-ends, -1, 1) }
+ bind "<ctrl>e" { "move-cursor" (paragraph-ends, 1, 0) }
+ bind "<shift><ctrl>e" { "move-cursor" (paragraph-ends, 1, 1) }
+
+ bind "<ctrl>w" { "cut-clipboard" () }
+ bind "<ctrl>y" { "paste-clipboard" () }
+
+ bind "<ctrl>d" { "delete-from-cursor" (chars, 1) }
+ bind "<alt>d" { "delete-from-cursor" (word-ends, 1) }
+ bind "<ctrl>k" { "delete-from-cursor" (paragraph-ends, 1) }
+ bind "<alt>backslash" { "delete-from-cursor" (whitespace, 1) }
+
+ bind "<alt>space" { "delete-from-cursor" (whitespace, 1)
+ "insert-at-cursor" (" ") }
+ bind "<alt>KP_Space" { "delete-from-cursor" (whitespace, 1)
+ "insert-at-cursor" (" ") }
+
+ #
+ # Some non-Emacs keybindings people are attached to
+ #
+ bind "<ctrl>u" {
+ "move-cursor" (paragraph-ends, -1, 0)
+ "delete-from-cursor" (paragraph-ends, 1)
+ }
+ bind "<ctrl>h" { "delete-from-cursor" (chars, -1) }
+ bind "<ctrl>w" { "delete-from-cursor" (word-ends, -1) }
+}
+
+#
+# Bindings for GtkTextView
+#
+binding "gtk-emacs-text-view"
+{
+# bind "<ctrl>p" { "move-cursor" (display-lines, -1, 0) }
+ bind "<shift><ctrl>p" { "move-cursor" (display-lines, -1, 1) }
+# bind "<ctrl>n" { "move-cursor" (display-lines, 1, 0) }
+ bind "<shift><ctrl>n" { "move-cursor" (display-lines, 1, 1) }
+
+ bind "<ctrl>space" { "set-anchor" () }
+ bind "<ctrl>KP_Space" { "set-anchor" () }
+}
+
+#
+# Bindings for GtkTreeView
+#
+binding "gtk-emacs-tree-view"
+{
+ bind "<ctrl>s" { "start-interactive-search" () }
+ bind "<ctrl>f" { "move-cursor" (logical-positions, 1) }
+ bind "<ctrl>b" { "move-cursor" (logical-positions, -1) }
+}
+
+class "GtkEntry" binding "gtk-emacs-text-entry"
+class "GtkTextView" binding "gtk-emacs-text-entry"
+class "GtkTextView" binding "gtk-emacs-text-view"
+class "GtkTreeView" binding "gtk-emacs-tree-view"
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+open MatitaGtkMisc
+open MatitaTypes
+open MatitaMisc
+
+(** {2 Initialization} *)
+
+let _ =
+ Helm_registry.load_from "matita.conf.xml"; (* read conf *)
+ Http_getter.init ();
+ MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+ MatitaDb.clean_owner_environment ();
+ MatitaDb.create_owner_environment ();
+ GtkMain.Rc.add_default_file BuildTimeConf.gtkrc; (* loads gtk rc files *)
+ ignore (GMain.Main.init ());
+
+ (* environment trust *)
+ CicEnvironment.set_trust
+ (let trust = Helm_registry.get_bool "matita.environment_trust" in
+ fun _ -> trust)
+
+(** {2 GUI callbacks} *)
+
+let gui = MatitaGui.instance ()
+
+let _ =
+ ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ ->
+ ignore (MatitaMathView.cicBrowser ())));
+ (* disambiguator callback *)
+ MatitaDisambiguator.set_choose_uris_callback
+ (MatitaGui.interactive_uri_choice ());
+ MatitaDisambiguator.set_choose_interp_callback
+ (MatitaGui.interactive_interp_choice ())
+
+let script =
+ MatitaScript.script ~buffer:gui#main#scriptTextView#buffer
+ ~init:(Lazy.force MatitaEngine.initial_status) ()
+
+ (* math viewers *)
+let _ =
+ let sequent_viewer = MatitaMathView.sequentViewer_instance () in
+ let sequents_viewer = MatitaMathView.sequentsViewer_instance () in
+ sequent_viewer#set_href_callback
+ (Some (fun uri -> (MatitaMathView.cicBrowser ())#loadUri uri));
+ let browser_observer _ = MatitaMathView.refresh_all_browsers () in
+ let sequents_observer status =
+ sequents_viewer#reset;
+ match status.proof_status with
+ | Incomplete_proof ((proof, goal) as status) ->
+ sequents_viewer#load_sequents status;
+ sequents_viewer#goto_sequent goal
+ | _ -> ()
+ in
+ script#addObserver sequents_observer;
+ script#addObserver browser_observer
+
+ (** <DEBUGGING> *)
+let _ =
+ if BuildTimeConf.debug then begin
+ gui#main#debugMenu#misc#show ();
+ let addDebugItem ~label callback =
+ let item =
+ GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label ()
+ in
+ ignore (item#connect#activate callback)
+ in
+ addDebugItem "dump environment to \"env.dump\"" (fun _ ->
+ let oc = open_out "env.dump" in
+ CicEnvironment.dump_to_channel oc;
+ close_out oc);
+ addDebugItem "print selected terms" (fun () ->
+ let i = ref 0 in
+ List.iter
+ (fun t ->
+ incr i;
+ MatitaLog.debug (sprintf "%d: %s" !i (CicPp.ppterm t)))
+ (MatitaMathView.sequentViewer_instance ())#get_selected_terms);
+ addDebugItem "dump getter settings" (fun _ ->
+ prerr_endline (Http_getter_env.env_to_string ()));
+ addDebugItem "getter: update"
+ (fun _ ->
+ ignore (Thread.create (fun () ->
+ MatitaLog.message "Rebuilding getter maps in background ...";
+ Http_getter.update ();
+ MatitaLog.message "Getter maps successfully rebuilt.") ()));
+ addDebugItem "getter: getalluris" (fun _ ->
+ List.iter prerr_endline (Http_getter.getalluris ()));
+ addDebugItem "dump script status" script#dump;
+ addDebugItem "dump metasenv"
+ (fun _ ->
+ if script#onGoingProof () then
+ MatitaLog.debug (CicMetaSubst.ppmetasenv script#proofMetasenv []));
+ addDebugItem "rotate light bulbs"
+ (fun _ ->
+ let nb = gui#main#hintNotebook in
+ nb#goto_page ((nb#current_page + 1) mod 3));
+ end
+
+ (** </DEBUGGING> *)
+
+let _ =
+ at_exit
+ (fun () ->
+ Http_getter_logger.log "Sync map tree to disk...";
+ Http_getter.sync_dump_file ();
+ print_endline "\nThanks for using Matita!\n");
+ Sys.catch_break true;
+ (try
+ script#loadFrom Sys.argv.(1);
+ with Invalid_argument _ -> ());
+ if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *)
+ Helm_registry.set "matita.mode" "cicbrowser";
+ let browser = MatitaMathView.cicBrowser () in
+ try
+ browser#loadUri Sys.argv.(1)
+ with Invalid_argument _ -> ()
+ end else begin (* matita *)
+ Helm_registry.set "matita.mode" "matita";
+ gui#main#mainWin#show ();
+ end;
+ try
+ GtkThread.main ()
+ with Sys.Break -> ()
+
--- /dev/null
+
+(**********************************************************************)
+
+TODO
+- implementare macro in matitaScript.ml (check, hint, ..) -> Gares
+- script outline -> Zack
+- cicBrowser: riagganciare(?) resa di termini scritti
+ nella URL(??) ->
+- menu contestuale (tasto dx) nel sequent viewer ->
+- controllo per script modificato o meno prima di uscire ->
+- riattaccare hbugs (brrr...) -> Zack
+- spostare il codice di creazione delle tabelle da
+ MatitaDb, al momento quelle create da matita possono
+ andare out of sync con quelle create dai file .sql
+
+DONE
+- tree update in background -> Gares
+- update del getter in background -> Zack
+- agganciare href_callback del sequent_viewer -> Zack
+- shortcut varie per script handling -> Zack
+- operazioni rimanenti su script (top, bottom, jump) -> Zack
+- lighting-ls-getter in matita -> Gares
+- riagganciare toolbar -> Zack
+- evitare che n-mila tattiche Goal siano nello script
+ (una per ogni cambio di tab) -> Zack
+- implementazione comandi rimanenti in matitaEngine.ml -> Gares
+- sintassi per gli alias -> Gares
+- implementazione script handling (sopra engine) -> Zack
+- matitaSync all'indietro -> Gares
+- riagganciare GUI -> Zack
+
+(**********************************************************************)
+
+comandi:
+ - interattivi (solo da gui)
+ - Macro/Comandi (check, print, hint, undo, locate, match)
+ potrebbero anche non avere sintassi concreta, del tipo che
+ check e' solo un bottone che apre una finetra in cui puoi
+ scrivere un termine o selezionarlo dalla prova corrente
+ - batch (sono gli unici che stanno nel .ma)
+ - Tattiche, theorem, alias (cambiano la prova)
+
+
+ MOUSE
+-------------------------------------------+
+ gui (macro: hint) | SHELL
+ (disambiguatore) |
+ +-----------------+---------------+-----------------------------------
+ | matita (status) | | matitac
+ | (log) (sync) | but2log | fold ( fun s l -> engine l s) file
+ +-----------------+---------------+-----------------------------------
+ | lingua:/sintassi concreta non ambigua delle tattiche+Qed,Thm,alias/
+ +----------------------------------------------------------
+ | engine: TacticAst (cic) -> status -> status
+ | ma non usa il campo alias dello status
+---------+----------------------------------------------------------
+ ocaml
+--------------------------------------------------------------------
+
+
+engine:
+ - accetta solo linee non ambigue
+ - alias:
+ alias ident nat = "cic:/matita/gares/nat.ind#(1/1)".
+ alias number = (natural|real|positive|integer).
+
+
+
+matita:
+ - mantiene uno stack di stati
+ - mantiene un log sync con gli stati
+ - offre delle api per generare la sintassi concreta che puo' servire
+ alla gui (la gui fa una chiamata a funzione e matita genera "auto."
+ cosi' la sintassi la gui non la vede mai e la tratta al massimo come un
+ testo semplice e basta (insomma, metterei in matita il generatore di
+ sintassi concreta) but2log
+ - ha il controllo... ovvero anche la gui viene usata da matita, o per sapere
+ la prossima azione o per chidere di scegliere il termine tra una lista
+
+ (stato :: tl) (log , (start,end) :: tl)
+
+ +----------+
+ | |
+ +----------+
+
+gui:
+ - step
+ - choose
+
+stato:
+ - alias
+ - proof status option
+ - metadati relativi allo script per il sync
+ - settings "baseuri/url/" eccc
+ -
+
+alias
+ - sintassi concreta
+
+engine prende in input
+ - AST di Cic (tactic ast)
+
+sync:
+ - presi 2 stati fa il diff e lo somma/sottrae al DB
+
+(**********************************************************************)
+
+script handling
+- ad ogni script sul quale l'utente sta lavorando corrispondono
+ - un modello (vedi sotto)
+ - un buffer di testo gtk + attributi (usati principalmente per distinguere la
+ parte di testo immodificabile da quella modificabile)
+ - una lista di observer che vengono notificati ad ogni cambiamento di stato
+- un modello di script e' composto da:
+ - una lista di stringhe (inizialmente vuota) detta "statement list". Ogni
+ elemento della lista corrisponde ad uno statement (nel senso di
+ TacticAst.statement) gia' valutato dall'engine. La parte immodificabile del
+ buffer di testo corrisponde con le stringhe contenute nella lista
+ - una lista di stati (inizialmente contenente lo stato vuoto) detta "state
+ list". Si ha l'invariante che la lunghezza di tale lista e' uguale alla
+ lunghezza della statements list + 1. Lo stato i-esimo della lista di stati
+ e' lo stato di matita _prima_ dell'esecuzione dell i-esimo statement
+ - una stringa, detta "future text", corrispondente alla parte di testo dello
+ script non ancora valutata. L'ultimo stato della state list e' lo stato
+ corrente di matita
+- relazione tra modello e buffer di testo gtk
+ - le modifiche al testo del buffer sono possibili solo nella parta non ancora
+ valutata. Ognuna di esse viene apportata _anche_ al future text
+ - invariante: e' sempre possibile riscrivere ("redraw") l'intero contenuto del
+ buffer di testo a partire dal modello, attributi compresi
+- oggetto script
+ - metodi
+ - new: gtk_text_buffer -> script
+ - redraw: unit (* ridisegna il contenuto del buffer di testo *)
+ - advance: ?statement:string -> unit -> unit
+ (* valuta il primo statement del future text (usando eval_statement
+ (puo' fallire con una eccezione)), rimuove il testo corrispondente dal
+ future text, aggiunge alla statement list una entry per ogni statement
+ ritornato da eval_statement, aggiunge il nuovo stato alla state list,
+ invoka tutti gli observer
+ Se c'e' l'argomento opzionale statement, quello e' il testo che viene
+ passato ad eval_statement, se ha successo nessuna rimozione dal future
+ text viene effettuata *)
+ - retract: unit -> unit
+ (* sposta l'ultimo statement della statement list al future text, toglie
+ l'ultimo stato della state list, MatitaSync.time_travel
+ ~present:ultimo_stato ~past:stato_precedente *)
+ - private eval_statement: string -> MatitaTypes.status * string list
+ (* parsa lo statement
+ - se e' un Command o un Tactical (vedi TacticAst) invoca MatitaEngine
+ passando lo stato corrente
+ - se e' una Macro la gestisce (= tutte le Macro sono implementate qua)
+ Ritorna una lista di coppie <stato, statement>. La proiezione sulla
+ prima componente rappresenta gli stati da aggiungere alla state list;
+ quella sulla seconda gli statement da aggiungere alla statement list.
+ *)
+ (* gestione degli observer *)
+ - add_observer: (MatitaTypes.status -> unit) -> observer_id
+ - remove_observer: observer_id -> unit
+ (* gestione del salvataggio *)
+ - save_to: string -> unit (* ridisegna su file *)
+ - load_from: string -> unit
+ (* retract fino allo stato zero, nuovo stato con future text pari al
+ contenuto del file passato *)
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf ;;
+
+let instance =
+ let dbd = lazy (
+ Mysql.quick_connect
+ ~host:(Helm_registry.get "db.host")
+ ~user:(Helm_registry.get "db.user")
+ ~database:(Helm_registry.get "db.database")
+ ())
+ in
+ fun () -> Lazy.force dbd
+
+
+let xpointer_RE = Pcre.regexp "#.*$"
+
+let clean_owner_environment () =
+ let dbd = instance () in
+ let owner = (Helm_registry.get "matita.owner") in
+ let obj_tbl = MetadataTypes.obj_tbl () in
+ let sort_tbl = MetadataTypes.sort_tbl () in
+ let rel_tbl = MetadataTypes.rel_tbl () in
+ let name_tbl = MetadataTypes.name_tbl () in
+ let conclno_tbl = MetadataTypes.conclno_tbl () in
+ let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in
+ let statements = [
+ sprintf "DROP TABLE %s ;" obj_tbl;
+ sprintf "DROP TABLE %s ;" sort_tbl;
+ sprintf "DROP TABLE %s ;" rel_tbl;
+ sprintf "DROP TABLE %s ;" name_tbl;
+ sprintf "DROP TABLE %s ;" conclno_tbl;
+ sprintf "DROP TABLE %s ;" conclno_hyp_tbl ] in
+(*
+DROP INDEX refObj_source ON refObj (source);
+DROP INDEX refObj_target ON refObj (h_occurrence);
+DROP INDEX refObj_position ON refObj (h_position);
+DROP INDEX refSort_source ON refSort (source);
+DROP INDEX objectName_value ON objectName (value);
+DROP INDEX no_inconcl_aux_source ON no_inconcl_aux (source);
+DROP INDEX no_inconcl_aux_no ON no_inconcl_aux (no);
+DROP INDEX no_concl_hyp_source ON no_concl_hyp (source);
+DROP INDEX no_concl_hyp_no ON no_concl_hyp (no);
+*)
+ let owned_uris =
+ try
+ MetadataDb.clean ~dbd
+ with Mysql.Error _ as exn ->
+ match Mysql.errno dbd with
+ | Mysql.No_such_table -> []
+ | _ -> raise exn
+ in
+ List.iter
+ (fun uri ->
+ let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in
+ List.iter
+ (fun suffix -> Http_getter.unregister (uri ^ suffix))
+ [""; ".body"; ".types"])
+ owned_uris;
+ List.iter (fun statement ->
+ try
+ ignore (Mysql.exec dbd statement)
+ with Mysql.Error _ as exn ->
+ match Mysql.errno dbd with
+ | Mysql.Bad_table_error -> ()
+ | _ -> raise exn
+ ) statements;
+;;
+
+let create_owner_environment () =
+ let dbd = instance () in
+ let owner = (Helm_registry.get "matita.owner") in
+ let obj_tbl = MetadataTypes.obj_tbl () in
+ let sort_tbl = MetadataTypes.sort_tbl () in
+ let rel_tbl = MetadataTypes.rel_tbl () in
+ let name_tbl = MetadataTypes.name_tbl () in
+ let conclno_tbl = MetadataTypes.conclno_tbl () in
+ let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in
+ let statements = [
+ sprintf "CREATE TABLE %s (
+ source varchar(255) binary not null,
+ h_occurrence varchar(255) binary not null,
+ h_position varchar(255) binary not null,
+ h_depth integer
+ );" obj_tbl;
+ sprintf "CREATE TABLE %s (
+ source varchar(255) binary not null,
+ h_position varchar(255) binary not null,
+ h_depth integer not null,
+ h_sort varchar(255) binary not null
+ );" sort_tbl;
+ sprintf "CREATE TABLE %s (
+ source varchar(255) binary not null,
+ h_position varchar(255) binary not null,
+ h_depth integer not null
+ );" rel_tbl;
+ sprintf "CREATE TABLE %s (
+ source varchar(255) binary not null,
+ value varchar(255) binary not null
+ );" name_tbl;
+ sprintf "CREATE TABLE %s (
+ source varchar(255) binary not null,
+ no tinyint(4) not null
+ );" conclno_tbl;
+ sprintf "CREATE TABLE %s (
+ source varchar(255) binary not null,
+ no tinyint(4) not null
+ );" conclno_hyp_tbl ] in
+(*
+CREATE INDEX refObj_source ON refObj (source);
+CREATE INDEX refObj_target ON refObj (h_occurrence);
+CREATE INDEX refObj_position ON refObj (h_position);
+CREATE INDEX refSort_source ON refSort (source);
+CREATE INDEX objectName_value ON objectName (value);
+CREATE INDEX no_inconcl_aux_source ON no_inconcl_aux (source);
+CREATE INDEX no_inconcl_aux_no ON no_inconcl_aux (no);
+CREATE INDEX no_concl_hyp_source ON no_concl_hyp (source);
+CREATE INDEX no_concl_hyp_no ON no_concl_hyp (no);
+*)
+ List.iter (fun statement ->
+ try
+ ignore (Mysql.exec dbd statement)
+ with
+ exn ->
+ let status = Mysql.status dbd in
+ match status with
+ | Mysql.StatusError Mysql.Table_exists_error -> ()
+ | Mysql.StatusError _ -> raise exn
+ | _ -> ()
+ ) statements
+;;
+
+(* removes uri from the ownerized tables, and returns the list of other objects
+ * (theyr uris) that ref the one removed.
+ * AFAIK there is no need to return it, since the MatitaTypes.staus should
+ * contain all defined objects. but to double ckeck we do not garbage the
+ * metadata...
+ *)
+let remove_uri uri =
+ let obj_tbl = MetadataTypes.obj_tbl () in
+ let sort_tbl = MetadataTypes.sort_tbl () in
+ let rel_tbl = MetadataTypes.rel_tbl () in
+ let name_tbl = MetadataTypes.name_tbl () in
+ let conclno_tbl = MetadataTypes.conclno_tbl () in
+ let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in
+ let dbd = instance () in
+ let suri = UriManager.string_of_uri uri in
+ let query table suri = sprintf
+ "DELETE FROM %s WHERE source LIKE '%s%%'" table (Mysql.escape suri)
+ in
+ List.iter (fun t ->
+ try
+ ignore (Mysql.exec dbd (query t suri))
+ with
+ exn -> raise exn (* no errors should be accepted *)
+ ) [obj_tbl;sort_tbl;rel_tbl;name_tbl;conclno_tbl;conclno_hyp_tbl];
+ (* and now the debug job *)
+ let dbg_q =
+ sprintf "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl suri
+ in
+ try
+ let rc = Mysql.exec dbd dbg_q in
+ let l = ref [] in
+ Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
+ let l = List.sort Pervasives.compare !l in
+ let rec uniq = function
+ | [] -> []
+ | h::[] -> [h]
+ | h1::h2::tl when h1 = h2 -> uniq (h2 :: tl)
+ | h1::tl (* when h1 <> h2 *) -> h1 :: uniq tl
+ in
+ uniq l
+ with
+ exn -> raise exn (* no errors should be accepted *)
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val instance: unit -> Mysql.dbd
+
+val clean_owner_environment : unit -> unit
+val create_owner_environment : unit -> unit
+
+val remove_uri: UriManager.uri -> string list
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+open MatitaTypes
+
+exception Ambiguous_input
+
+type choose_uris_callback = id:string -> string list -> string list
+type choose_interp_callback = (string * string) list list -> int list
+
+let mono_uris_callback ~id = raise Ambiguous_input
+let mono_interp_callback _ = raise Ambiguous_input
+
+let _choose_uris_callback = ref mono_uris_callback
+let _choose_interp_callback = ref mono_interp_callback
+let set_choose_uris_callback f = _choose_uris_callback := f
+let set_choose_interp_callback f = _choose_interp_callback := f
+
+module Callbacks =
+ struct
+ let interactive_user_uri_choice ~selection_mode ?ok
+ ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
+ !_choose_uris_callback ~id uris
+
+ let interactive_interpretation_choice interp =
+ !_choose_interp_callback interp
+
+ let input_or_locate_uri ~(title:string) ?id =
+ (* Zack: I try to avoid using this callback. I therefore assume that
+ * the presence of an identifier that can't be resolved via "locate"
+ * query is a syntax error *)
+ let msg = match id with Some id -> id | _ -> "_" in
+ raise (Unbound_identifier msg)
+ end
+
+module Disambiguator = Disambiguate.Make (Callbacks)
+
+(* implement module's API *)
+
+let disambiguate_term = Disambiguator.disambiguate_term
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open MatitaTypes
+
+(** raised when ambiguous input is found but not expected (e.g. in the batch
+ * compiler) *)
+exception Ambiguous_input
+
+type choose_uris_callback = id:string -> string list -> string list
+type choose_interp_callback = (string * string) list list -> int list
+
+val set_choose_uris_callback: choose_uris_callback -> unit
+val set_choose_interp_callback: choose_interp_callback -> unit
+
+(** @raise Ambiguous_input if called, default value for internal
+ * choose_uris_callback if not set otherwise with set_choose_uris_callback
+ * above *)
+val mono_uris_callback: choose_uris_callback
+
+(** @raise Ambiguous_input if called, default value for internal
+ * choose_interp_callback if not set otherwise with set_choose_interp_callback
+ * above *)
+val mono_interp_callback: choose_interp_callback
+
+(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *)
+
+include Disambiguate.Disambiguator
+ (*
+ * val disambiguate_term: ...
+ *)
+
--- /dev/null
+
+open Printf
+
+open MatitaTypes
+
+
+(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
+ * names as long as they are available, then it fallbacks to name generation
+ * using FreshNamesGenerator module *)
+let namer_of names =
+ let len = List.length names in
+ let count = ref 0 in
+ fun metasenv context name ~typ ->
+ if !count < len then begin
+ let name = Cic.Name (List.nth names !count) in
+ incr count;
+ name
+ end else
+ FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
+
+let tactic_of_ast = function
+ | TacticAst.Intros (_, _, names) ->
+ (* TODO Zack implement intros length *)
+ PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
+ | TacticAst.Reflexivity _ -> Tactics.reflexivity
+ | TacticAst.Assumption _ -> Tactics.assumption
+ | TacticAst.Contradiction _ -> Tactics.contradiction
+ | TacticAst.Exists _ -> Tactics.exists
+ | TacticAst.Fourier _ -> Tactics.fourier
+ | TacticAst.Goal (_, n) -> Tactics.set_goal n
+ | TacticAst.Left _ -> Tactics.left
+ | TacticAst.Right _ -> Tactics.right
+ | TacticAst.Ring _ -> Tactics.ring
+ | TacticAst.Split _ -> Tactics.split
+ | TacticAst.Symmetry _ -> Tactics.symmetry
+ | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
+ | TacticAst.Apply (_, term) -> Tactics.apply term
+ | TacticAst.Absurd (_, term) -> Tactics.absurd term
+ | TacticAst.Exact (_, term) -> Tactics.exact term
+ | TacticAst.Cut (_, term) -> Tactics.cut term
+ | TacticAst.Elim (_, term, _) ->
+ (* TODO Zack implement "using" argument *)
+ Tactics.elim_intros_simpl term
+ | TacticAst.ElimType (_, term) -> Tactics.elim_type term
+ | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
+(* | TacticAst.Auto _ -> Tactics.auto_new ~dbd *)
+ | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
+(*
+ (* TODO Zack a lot more of tactics to be implemented here ... *)
+ | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
+ | TacticAst.Change of 'term * 'term * 'ident option
+ | TacticAst.Decompose of 'ident * 'ident list
+ | TacticAst.Discriminate of 'ident
+ | TacticAst.Fold of reduction_kind * 'term
+ | TacticAst.Injection of 'ident
+ | TacticAst.LetIn of 'term * 'ident
+ | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
+ | TacticAst.Replace_pattern of 'term pattern * 'term
+ | TacticAst.Rewrite of direction * 'term * 'ident option
+*)
+ | _ -> assert false
+
+let eval_tactical status tac =
+ let apply_tactic tactic =
+ let (proof, goals) =
+ ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
+ in
+ let new_status =
+ match goals with
+ | [] ->
+ let (_,metasenv,_,_) = proof in
+ (match metasenv with
+ | [] -> Proof proof
+ | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
+ | ng::_ -> Incomplete_proof (proof, ng)
+ in
+ { status with proof_status = new_status }
+ in
+ let rec tactical_of_ast = function
+ | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
+ | TacticAst.Fail loc -> Tacticals.fail
+ | TacticAst.Do (loc, num, tactical) ->
+ Tacticals.do_tactic num (tactical_of_ast tactical)
+ | TacticAst.IdTac loc -> Tacticals.id_tac
+ | TacticAst.Repeat (loc, tactical) ->
+ Tacticals.repeat_tactic (tactical_of_ast tactical)
+ | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
+ Tacticals.seq (List.map tactical_of_ast tacticals)
+ | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
+ Tacticals.thens (tactical_of_ast tactical)
+ (List.map tactical_of_ast tacticals)
+ | TacticAst.Tries (loc, tacticals) ->
+ Tacticals.try_tactics
+ (List.map (fun t -> "", tactical_of_ast t) tacticals)
+ | TacticAst.Try (loc, tactical) ->
+ Tacticals.try_tactic (tactical_of_ast tactical)
+ in
+ apply_tactic (tactical_of_ast tac)
+
+let eval_command status cmd =
+ match cmd with
+ | TacticAst.Set (loc, name, value) -> set_option status name value
+ | TacticAst.Qed loc ->
+ let uri, metasenv, bo, ty =
+ match status.proof_status with
+ | Proof (Some uri, metasenv, body, ty) ->
+ uri, metasenv, body, ty
+ | Proof (None, metasenv, body, ty) ->
+ command_error
+ ("Someone allows to start a thm without giving the "^
+ "name/uri. This should be fixed!")
+ | _-> command_error "You can't qed an uncomplete theorem"
+ in
+ let suri = UriManager.string_of_uri uri in
+ if metasenv <> [] then
+ command_error "Proof not completed! metasenv is not empty!";
+ let proved_ty,ugraph =
+ CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
+ in
+ let b,ugraph =
+ CicReduction.are_convertible [] proved_ty ty ugraph
+ in
+ if not b then
+ command_error
+ ("The type of your proof is not convertible with the "^
+ "type you've declared!");
+ MatitaLog.message (sprintf "%s defined" suri);
+ let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
+ {status with proof_status = No_proof }
+ | TacticAst.Inductive (loc, dummy_params, types) ->
+ (* dummy_params are not real params, it is a list of nothing, and the only
+ * semantic content is the len, that is leftno (note: leftno and pamaters
+ * have nothing in common).
+ *)
+ let suri =
+ match types with
+ | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
+ | _ -> assert false
+ in
+ let uri = UriManager.uri_of_string suri in
+ let leftno = List.length dummy_params in
+ let obj = Cic.InductiveDefinition (types, [], leftno, []) in
+ let ugraph =
+ CicTypeChecker.typecheck_mutual_inductive_defs uri
+ (types, [], leftno) CicUniv.empty_ugraph
+ in
+ MatitaSync.add_inductive_def
+ ~uri ~types ~params:[] ~leftno ~ugraph status;
+ | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
+ let uri =
+ UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
+ in
+ let goalno = 1 in
+ let metasenv, body =
+ match status.proof_status with
+ | Intermediate metasenv ->
+ ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
+ | _-> assert false
+ in
+ let initial_proof = (Some uri, metasenv, body, ty) in
+ { status with proof_status = Incomplete_proof (initial_proof,goalno)}
+ | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
+ let uri =
+ UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
+ in
+ let metasenv = MatitaMisc.get_proof_metasenv status in
+ let (body_type, ugraph) =
+ CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
+ in
+ let (subst, metasenv, ugraph) =
+ CicUnification.fo_unif metasenv [] body_type ty ugraph
+ in
+ if metasenv <> [] then
+ command_error
+ "metasenv not empty while giving a definition with body";
+ let body = CicMetaSubst.apply_subst subst body in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ MatitaSync.add_constant ~uri ~body ~ty ~ugraph status
+ | TacticAst.Theorem (_, _, None, _, _) ->
+ command_error "The grammas should avoid having unnamed theorems!"
+ | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
+ | TacticAst.Alias (loc, spec) ->
+ match spec with
+ | TacticAst.Ident_alias (id,uri) ->
+ {status with aliases =
+ DisambiguateTypes.Environment.add
+ (DisambiguateTypes.Id id)
+ ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
+ status.aliases }
+ | TacticAst.Symbol_alias (symb, instance, desc) ->
+ {status with aliases =
+ DisambiguateTypes.Environment.add
+ (DisambiguateTypes.Symbol (symb,instance))
+ (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
+ status.aliases }
+ | TacticAst.Number_alias (instance,desc) ->
+ {status with aliases =
+ DisambiguateTypes.Environment.add
+ (DisambiguateTypes.Num instance)
+ (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
+
+let eval status st =
+ match st with
+ | TacticAst.Tactical (_, tac) -> eval_tactical status tac
+ | TacticAst.Command (_, cmd) -> eval_command status cmd
+ | TacticAst.Macro (_, mac) ->
+ command_error (sprintf "The macro %s can't be in a script"
+ (TacticAstPp.pp_macro_cic mac))
+
+let disambiguate_term status term =
+ let (aliases, metasenv, cic, _) =
+ match
+ MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
+ ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
+ ~metasenv:(MatitaMisc.get_proof_metasenv status) term
+ with
+ | [x] -> x
+ | _ -> assert false
+ in
+ let proof_status =
+ match status.proof_status with
+ | No_proof -> Intermediate metasenv
+ | Incomplete_proof ((uri, _, proof, ty), goal) ->
+ Incomplete_proof ((uri, metasenv, proof, ty), goal)
+ | Intermediate _ -> Intermediate metasenv
+ | Proof _ -> assert false
+ in
+ let status =
+ { status with
+ aliases = aliases;
+ proof_status = proof_status }
+ in
+ status, cic
+
+let disambiguate_terms status terms =
+ let term = CicAst.pack terms in
+ let status, term = disambiguate_term status term in
+ status, CicUtil.unpack term
+
+let disambiguate_tactic status = function
+ | TacticAst.Transitivity (loc, term) ->
+ let status, cic = disambiguate_term status term in
+ status, TacticAst.Transitivity (loc, cic)
+ | TacticAst.Apply (loc, term) ->
+ let status, cic = disambiguate_term status term in
+ status, TacticAst.Apply (loc, cic)
+ | TacticAst.Absurd (loc, term) ->
+ let status, cic = disambiguate_term status term in
+ status, TacticAst.Absurd (loc, cic)
+ | TacticAst.Exact (loc, term) ->
+ let status, cic = disambiguate_term status term in
+ status, TacticAst.Exact (loc, cic)
+ | TacticAst.Cut (loc, term) ->
+ let status, cic = disambiguate_term status term in
+ status, TacticAst.Cut (loc, cic)
+ | TacticAst.Elim (loc, term, Some term') ->
+ let status, cic1 = disambiguate_term status term in
+ let status, cic2 = disambiguate_term status term' in
+ status, TacticAst.Elim (loc, cic1, Some cic2)
+ | TacticAst.Elim (loc, term, None) ->
+ let status, cic = disambiguate_term status term in
+ status, TacticAst.Elim (loc, cic, None)
+ | TacticAst.ElimType (loc, term) ->
+ let status, cic = disambiguate_term status term in
+ status, TacticAst.ElimType (loc, cic)
+ | TacticAst.Replace (loc, what, with_what) ->
+ let status, cic1 = disambiguate_term status what in
+ let status, cic2 = disambiguate_term status with_what in
+ status, TacticAst.Replace (loc, cic1, cic2)
+ | TacticAst.Change (loc, what, with_what, ident) ->
+ let status, cic1 = disambiguate_term status what in
+ let status, cic2 = disambiguate_term status with_what in
+ status, TacticAst.Change (loc, cic1, cic2, ident)
+(*
+ (* TODO Zack a lot more of tactics to be implemented here ... *)
+ | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
+ | TacticAst.Change of 'term * 'term * 'ident option
+ | TacticAst.Decompose of 'ident * 'ident list
+ | TacticAst.Discriminate of 'ident
+ | TacticAst.Fold of reduction_kind * 'term
+ | TacticAst.Injection of 'ident
+ | TacticAst.LetIn of 'term * 'ident
+ | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
+ | TacticAst.Replace_pattern of 'term pattern * 'term
+ | TacticAst.Rewrite of direction * 'term * 'ident option
+*)
+ | TacticAst.Intros (loc, num, names) ->
+ status, TacticAst.Intros (loc, num, names)
+ | TacticAst.Auto loc -> status, TacticAst.Auto loc
+ | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
+ | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
+ | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
+ | TacticAst.Exists loc -> status, TacticAst.Exists loc
+ | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
+ | TacticAst.Left loc -> status, TacticAst.Left loc
+ | TacticAst.Right loc -> status, TacticAst.Right loc
+ | TacticAst.Ring loc -> status, TacticAst.Ring loc
+ | TacticAst.Split loc -> status, TacticAst.Split loc
+ | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
+ | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
+ | x ->
+ print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
+ assert false
+
+let rec disambiguate_tactical status = function
+ | TacticAst.Tactic (loc, tactic) ->
+ let status, tac = disambiguate_tactic status tactic in
+ status, TacticAst.Tactic (loc, tac)
+ | TacticAst.Do (loc, num, tactical) ->
+ let status, tac = disambiguate_tactical status tactical in
+ status, TacticAst.Do (loc, num, tac)
+ | TacticAst.Repeat (loc, tactical) ->
+ let status, tac = disambiguate_tactical status tactical in
+ status, TacticAst.Repeat (loc, tac)
+ | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
+ let status, tacticals = disambiguate_tacticals status tacticals in
+ let tacticals = List.rev tacticals in
+ status, TacticAst.Seq (loc, tacticals)
+ | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
+ let status, tactical = disambiguate_tactical status tactical in
+ let status, tacticals = disambiguate_tacticals status tacticals in
+ status, TacticAst.Then (loc, tactical, tacticals)
+ | TacticAst.Tries (loc, tacticals) ->
+ let status, tacticals = disambiguate_tacticals status tacticals in
+ status, TacticAst.Tries (loc, tacticals)
+ | TacticAst.Try (loc, tactical) ->
+ let status, tactical = disambiguate_tactical status tactical in
+ status, TacticAst.Try (loc, tactical)
+ | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
+ status, tac
+
+and disambiguate_tacticals status tacticals =
+ let status, tacticals =
+ List.fold_left
+ (fun (status, tacticals) tactical ->
+ let status, tac = disambiguate_tactical status tactical in
+ status, tac :: tacticals)
+ (status, [])
+ tacticals
+ in
+ let tacticals = List.rev tacticals in
+ status, tacticals
+
+let disambiguate_inddef status params indTypes =
+ let add_pi binders t =
+ List.fold_right
+ (fun (name, ast) acc ->
+ CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
+ binders t
+ in
+ let ind_binders =
+ List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
+ in
+ let binders = ind_binders @ params in
+ let asts = ref [] in
+ let add_ast ast = asts := ast :: !asts in
+ let paramsno = List.length params in
+ let indbindersno = List.length ind_binders in
+ List.iter
+ (fun (name, _, typ, constructors) ->
+ add_ast (add_pi params typ);
+ List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
+ indTypes;
+ let status, terms = disambiguate_terms status !asts in
+ let terms = ref (List.rev terms) in
+ let get_term () =
+ match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
+ in
+ let uri =
+ match indTypes with
+ | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
+ | _ -> assert false
+ in
+ let mutinds =
+ let counter = ref 0 in
+ List.map
+ (fun _ ->
+ incr counter;
+ CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
+ indTypes
+ in
+ let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
+ let cicIndTypes =
+ List.fold_left
+ (fun acc (name, inductive, typ, constructors) ->
+ let cicTyp = get_term () in
+ let cicConstructors =
+ List.fold_left
+ (fun acc (name, _) ->
+ let typ =
+ subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
+ in
+ (name, typ) :: acc)
+ [] constructors
+ in
+ (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
+ [] indTypes
+ in
+ let cicIndTypes = List.rev cicIndTypes in
+ status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
+
+let disambiguate_command status = function
+ | TacticAst.Inductive (loc, params, types) ->
+ let (status, (uri, (ind_types, vars, paramsno))) =
+ disambiguate_inddef status params types
+ in
+ let rec mk_list = function
+ | 0 -> []
+ | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
+ in
+ (* once we've built the cic inductive types we no longer need terms
+ corresponding to parameters, but we need the leftno, and we encode
+ it as the length of dummy_params
+ *)
+ let dummy_params = mk_list paramsno in
+ status, TacticAst.Inductive (loc, dummy_params, ind_types)
+ | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
+ let status, ty = disambiguate_term status ty in
+ let status, body =
+ match body with
+ | None -> status, None
+ | Some body ->
+ let status, body = disambiguate_term status body in
+ status, Some body
+ in
+ status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
+ | TacticAst.Coercion (loc, term) -> assert false (** TODO *)
+ | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
+ status, cmd
+ | TacticAst.Alias _ as x -> status, x
+
+let disambiguate_statement status statement =
+ match statement with
+ | TacticAst.Tactical (loc, tac) ->
+ let status, tac = disambiguate_tactical status tac in
+ status, (TacticAst.Tactical (loc, tac))
+ | TacticAst.Command (loc, cmd) ->
+ let status, cmd = disambiguate_command status cmd in
+ status, (TacticAst.Command (loc, cmd))
+ | TacticAst.Macro (_, mac) ->
+ command_error
+ (sprintf ("The engine is not allowed to disambiguate any macro, "^^
+ "in particular %s") (TacticAstPp.pp_macro_ast mac))
+
+let eval_ast status ast =
+ let status,st = disambiguate_statement status ast in
+ (* this disambiguation step should be deferred to support tacticals *)
+ eval status st
+
+let eval_from_stream status str =
+ let st = CicTextualParser2.parse_statement str in
+ eval_ast status st
+
+let eval_string status str =
+ eval_from_stream status (Stream.of_string str)
+
+let default_options () =
+ let options =
+ StringMap.add "baseuri"
+ (String
+ (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
+ no_options
+ in
+ let options =
+ StringMap.add "basedir"
+ (String (Helm_registry.get "matita.basedir" ))
+ options
+ in
+ options
+
+let initial_status =
+ lazy {
+ aliases = DisambiguateTypes.empty_environment;
+ proof_status = No_proof;
+ options = default_options ();
+ coercions = [];
+ objects = [];
+ }
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(*val eval_ast:*)
+
+val eval_string: MatitaTypes.status -> string -> MatitaTypes.status
+
+val eval_from_stream: MatitaTypes.status -> char Stream.t -> MatitaTypes.status
+
+val eval_ast:
+ MatitaTypes.status -> (CicAst.term, string) TacticAst.statement ->
+ MatitaTypes.status
+
+val eval:
+ MatitaTypes.status -> (Cic.term, string) TacticAst.statement ->
+ MatitaTypes.status
+
+val initial_status: MatitaTypes.status lazy_t
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+open MatitaTypes
+
+let wrap_callback f = f
+(*
+let wrap_callback f () =
+ try
+ f ()
+ with exn ->
+ MatitaLog.error (sprintf "Uncaught exception: %s" (Printexc.to_string exn))
+*)
+
+let connect_button (button: #GButton.button) callback =
+ ignore (button#connect#clicked (wrap_callback callback))
+
+let connect_menu_item (menu_item: #GMenu.menu_item) callback =
+ ignore (menu_item#connect#activate (wrap_callback callback))
+
+let connect_key (ev:GObj.event_ops) ?(modifiers = []) ?(stop = false) key
+ callback
+=
+ ignore (ev#connect#key_press (fun key' ->
+ let modifiers' = GdkEvent.Key.state key' in
+ (match key' with
+ | key' when GdkEvent.Key.keyval key' = key
+ && List.for_all (fun m -> List.mem m modifiers') modifiers ->
+ callback ();
+ stop
+ | _ -> false)))
+
+let toggle_visibility ~(win: GWindow.window) ~(check: GMenu.check_menu_item) =
+ ignore (check#connect#toggled (fun _ ->
+ if check#active then win#show () else win#misc#hide ()));
+ ignore (win#event#connect#delete (fun _ ->
+ win#misc#hide ();
+ check#set_active false;
+ true))
+
+let toggle_win ?(check: GMenu.check_menu_item option) (win: GWindow.window) () =
+ if win#is_active then win#misc#hide () else win#show ();
+ match check with
+ | None -> ()
+ | Some check -> check#set_active (not check#active)
+
+let add_key_binding key callback (evbox: GBin.event_box) =
+ ignore (evbox#event#connect#key_press (function
+ | key' when GdkEvent.Key.keyval key' = key ->
+ callback ();
+ false
+ | _ -> false))
+
+class stringListModel (tree_view: GTree.view) =
+ let column_list = new GTree.column_list in
+ let text_column = column_list#add Gobject.Data.string in
+ let list_store = GTree.list_store column_list in
+ object (self)
+
+ initializer
+ let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in
+ let view_column = GTree.view_column ~renderer () in
+ tree_view#set_model (Some (list_store :> GTree.model));
+ ignore (tree_view#append_column view_column)
+
+ method list_store = list_store
+
+ method easy_append s =
+ let tree_iter = list_store#append () in
+ list_store#set ~row:tree_iter ~column:text_column s
+
+ method easy_insert pos s =
+ let tree_iter = list_store#insert pos in
+ list_store#set ~row:tree_iter ~column:text_column s
+
+ method easy_selection () =
+ List.map
+ (fun tree_path ->
+ let iter = list_store#get_iter tree_path in
+ list_store#get ~row:iter ~column:text_column)
+ tree_view#selection#get_selected_rows
+
+ end
+
+class type gui =
+ object
+ method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+ method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog
+ method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
+ method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
+ end
+
+let ask_confirmation ~(gui:#gui) ?(cancel = true) ?(title = "") ?(msg = "") () =
+ let dialog = gui#newConfirmationDialog () in
+ dialog#confirmationDialog#set_title title;
+ dialog#confirmationDialogLabel#set_label msg;
+ let result = ref None in
+ let return r _ =
+ result := Some r;
+ dialog#confirmationDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true));
+ connect_button dialog#confirmationDialogOkButton (return true);
+ connect_button dialog#confirmationDialogCancelButton (return false);
+ if not cancel then dialog#confirmationDialogCancelButton#misc#hide ();
+ dialog#confirmationDialog#show ();
+ GtkThread.main ();
+ (match !result with None -> assert false | Some r -> r)
+
+let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () =
+ let dialog = gui#newEmptyDialog () in
+ dialog#emptyDialog#set_title title;
+ dialog#emptyDialogLabel#set_label msg;
+ let result = ref None in
+ let return r =
+ result := r;
+ dialog#emptyDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (dialog#emptyDialog#event#connect#delete (fun _ -> true));
+ if multiline then begin (* multiline input required: use a TextView widget *)
+ let win =
+ GBin.scrolled_window ~width:400 ~height:150 ~hpolicy:`NEVER
+ ~vpolicy:`ALWAYS ~packing:dialog#emptyDialogVBox#add ()
+ in
+ let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in
+ view#misc#grab_focus ();
+ connect_button dialog#emptyDialogOkButton (fun _ ->
+ return (Some (view#buffer#get_text ())))
+ end else begin (* monoline input required: use a TextEntry widget *)
+ let entry = GEdit.entry ~packing:dialog#emptyDialogVBox#add () in
+ entry#misc#grab_focus ();
+ connect_button dialog#emptyDialogOkButton (fun _ ->
+ return (Some entry#text))
+ end;
+ connect_button dialog#emptyDialogCancelButton (fun _ ->return None);
+ dialog#emptyDialog#show ();
+ GtkThread.main ();
+ (match !result with None -> raise Cancel | Some r -> r)
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(** {2 Gtk helpers} *)
+
+ (** given a window and a check menu item it links the two so that the former
+ * is only hidden on delete and the latter toggle show/hide of the former *)
+val toggle_visibility:
+ win:GWindow.window -> check:GMenu.check_menu_item -> unit
+
+val toggle_win:
+ ?check:GMenu.check_menu_item -> GWindow.window -> unit -> unit
+
+val add_key_binding: Gdk.keysym -> (unit -> 'a) -> GBin.event_box -> unit
+
+(** Connect a callback to the clicked signal of a button, ignoring its return
+ * value *)
+val connect_button: #GButton.button -> (unit -> unit) -> unit
+
+(** Like connect_button above, but connects a callback to the activate signal of
+ * a menu item *)
+val connect_menu_item: #GMenu.menu_item -> (unit -> unit) -> unit
+
+ (** connect a unit -> unit callback to a particular key press event. Event can
+ * be specified using its keysym and a list of modifiers which must be in
+ * effect for the callback to be executed. Further signal processing of other
+ * key press events remains unchanged; further signal processing of the
+ * specified key press depends on the stop parameter *)
+val connect_key:
+ GObj.event_ops ->
+ ?modifiers:Gdk.Tags.modifier list ->
+ ?stop:bool -> (* stop signal handling when the given key has been pressed?
+ * Defaults to false *)
+ Gdk.keysym -> (* (= int) the key, see GdkKeysyms.ml *)
+ (unit -> unit) -> (* callback *)
+ unit
+
+ (** single string column list *)
+class stringListModel:
+ GTree.view ->
+ object
+ method list_store: GTree.list_store (** list_store forwarding *)
+
+ method easy_append: string -> unit (** append + set *)
+ method easy_insert: int -> string -> unit (** insert + set *)
+ method easy_selection: unit -> string list
+ end
+
+(** {2 Matita GUI components} *)
+
+class type gui =
+ object (* minimal gui object requirements *)
+ method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+ method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog
+ method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
+ method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
+ end
+
+ (** {3 Dialogs} *)
+
+ (** @return true if user hit "ok" button, false if user hit "cancel" button
+ * @param cancel if set to true a cancel button is shown to the user, otherwise
+ * it is not (and indeed the function will return true). Defaults to true *)
+val ask_confirmation:
+ gui:#gui ->
+ ?cancel:bool -> ?title:string -> ?msg:string -> unit ->
+ bool
+
+ (** @param multiline (default: false) if true a TextView widget will be used
+ * for prompting the user otherwise a TextEntry widget will be
+ * @return the string given by the user *)
+val ask_text:
+ gui:#gui -> ?title:string -> ?msg:string -> ?multiline:bool -> unit -> string
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+open MatitaGeneratedGui
+open MatitaGtkMisc
+open MatitaMisc
+
+let gui_instance = ref None ;;
+
+class console ~(buffer: GText.buffer) () =
+ object (self)
+ val error_tag = buffer#create_tag [ `FOREGROUND "red" ]
+ val warning_tag = buffer#create_tag [ `FOREGROUND "yellow" ]
+ val message_tag = buffer#create_tag []
+ val debug_tag = buffer#create_tag [ `FOREGROUND "#888888" ]
+ method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s
+ method error s = buffer#insert ~iter:buffer#end_iter ~tags:[error_tag] s
+ method warning s = buffer#insert ~iter:buffer#end_iter ~tags:[warning_tag] s
+ method debug s = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s
+ method clear () =
+ buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
+ method log_callback (tag: MatitaLog.log_tag) s =
+ match tag with
+ | `Debug -> self#debug (s ^ "\n")
+ | `Error -> self#error (s ^ "\n")
+ | `Message -> self#message (s ^ "\n")
+ | `Warning -> self#warning (s ^ "\n")
+ end
+
+class gui () =
+ (* creation order _is_ relevant for windows placement *)
+ let main = new mainWin () in
+ let about = new aboutWin () in
+ let fileSel = new fileSelectionWin () in
+ let keyBindingBoxes = (* event boxes which should receive global key events *)
+ [ main#mainWinEventBox ]
+ in
+ let console = new console ~buffer:main#logTextView#buffer () in
+ object (self)
+ val mutable chosen_file = None
+ val mutable _ok_not_exists = false
+
+ initializer
+ (* glade's check widgets *)
+ List.iter (fun w -> w#check_widgets ())
+ (let c w = (w :> <check_widgets: unit -> unit>) in
+ [ c about; c fileSel; c main ]);
+ (* key bindings *)
+ List.iter (* global key bindings *)
+ (fun (key, callback) -> self#addKeyBinding key callback)
+(*
+ [ GdkKeysyms._F3,
+ toggle_win ~check:main#showProofMenuItem proof#proofWin;
+ GdkKeysyms._F4,
+ toggle_win ~check:main#showCheckMenuItem check#checkWin;
+*)
+ [ ];
+ (* about win *)
+ ignore (about#aboutWin#event#connect#delete (fun _ -> true));
+ ignore (main#aboutMenuItem#connect#activate (fun _ ->
+ about#aboutWin#show ()));
+ connect_button about#aboutDismissButton (fun _ ->
+ about#aboutWin#misc#hide ());
+ about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
+ ~templ:BuildTimeConf.version about#aboutLabel#label);
+ (* file selection win *)
+ ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
+ ignore (fileSel#fileSelectionWin#connect#response (fun event ->
+ let return r =
+ chosen_file <- r;
+ fileSel#fileSelectionWin#misc#hide ();
+ GMain.Main.quit ()
+ in
+ match event with
+ | `OK ->
+ let fname = fileSel#fileSelectionWin#filename in
+ if Sys.file_exists fname then
+ (if is_regular fname then return (Some fname))
+ else
+ (if _ok_not_exists then return (Some fname))
+ | `CANCEL -> return None
+ | `HELP -> ()
+ | `DELETE_EVENT -> return None));
+ (* menus *)
+ List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
+ main#helpMenu#set_right_justified true;
+ (* console *)
+ let adj = main#logScrolledWin#vadjustment in
+ ignore (adj#connect#changed
+ (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
+ console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
+ (* toolbar *)
+ let module A = TacticAst in
+ let hole = CicAst.UserInput in
+ let loc = CicAst.dummy_floc in
+ let tac ast _ =
+ if (MatitaScript.instance ())#onGoingProof () then
+ (MatitaScript.instance ())#advance
+ ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) ()
+ in
+ let tac_w_term ast _ =
+ if (MatitaScript.instance ())#onGoingProof () then
+ let (buf: GText.buffer) = self#main#scriptTextView#buffer in
+ buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
+ ("\n" ^ TacticAstPp.pp_tactic ast)
+ in
+ let tbar = self#main in
+ connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
+ connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
+ connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
+ connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None)));
+ connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole)));
+ connect_button tbar#splitButton (tac (A.Split loc));
+ connect_button tbar#leftButton (tac (A.Left loc));
+ connect_button tbar#rightButton (tac (A.Right loc));
+ connect_button tbar#existsButton (tac (A.Exists loc));
+ connect_button tbar#reflexivityButton (tac (A.Reflexivity loc));
+ connect_button tbar#symmetryButton (tac (A.Symmetry loc));
+ connect_button tbar#transitivityButton
+ (tac_w_term (A.Transitivity (loc, hole)));
+ connect_button tbar#assumptionButton (tac (A.Assumption loc));
+ connect_button tbar#cutButton (tac_w_term (A.Cut (loc, hole)));
+ connect_button tbar#autoButton (tac (A.Auto loc));
+ (* quit *)
+ self#setQuitCallback (fun () -> exit 0);
+ (* log *)
+ MatitaLog.set_log_callback self#console#log_callback;
+ GtkSignal.user_handler :=
+ (fun exn ->
+ MatitaLog.error
+ (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
+ (* script *)
+ let s () = MatitaScript.instance () in
+ let script_fname = ref None in
+ let enable_save_to f =
+ script_fname := Some f;
+ self#main#saveMenuItem#misc#set_sensitive true
+ in
+ let disable_save () =
+ script_fname := None;
+ self#main#saveMenuItem#misc#set_sensitive false
+ in
+ let loadScript () =
+ let script = s () in
+ match self#chooseFile () with
+ | Some f -> script#reset (); script#loadFrom f; enable_save_to f
+ | None -> ()
+ in
+ let saveAsScript () =
+ let script = s () in
+ match self#chooseFile ~ok_not_exists:true () with
+ | Some f -> script#saveTo f; enable_save_to f
+ | None -> ()
+ in
+ let saveScript () =
+ match !script_fname with
+ | None -> saveAsScript ()
+ | Some f -> (s ())#saveTo f
+ in
+ let newScript () = (s ())#reset (); disable_save () in
+ let cursor () =
+ let buf = self#main#scriptTextView#buffer in
+ buf#place_cursor (buf#get_iter_at_mark (`NAME "locked"))
+ in
+ let advance _ = (MatitaScript.instance ())#advance (); cursor () in
+ let retract _ = (MatitaScript.instance ())#retract (); cursor () in
+ let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
+ let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
+ let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
+ let connect_key sym f =
+ connect_key self#main#mainWinEventBox#event
+ ~modifiers:[`CONTROL] ~stop:true sym f;
+ connect_key self#main#scriptTextView#event
+ ~modifiers:[`CONTROL] ~stop:true sym f
+ in
+ connect_button self#main#scriptAdvanceButton advance;
+ connect_button self#main#scriptRetractButton retract;
+ connect_button self#main#scriptTopButton top;
+ connect_button self#main#scriptBottomButton bottom;
+ connect_key GdkKeysyms._Down advance;
+ connect_key GdkKeysyms._Up retract;
+ connect_key GdkKeysyms._Home top;
+ connect_key GdkKeysyms._End bottom;
+ connect_button self#main#scriptJumpButton jump;
+ connect_menu_item self#main#openMenuItem loadScript;
+ connect_menu_item self#main#saveMenuItem saveScript;
+ connect_menu_item self#main#saveAsMenuItem saveAsScript;
+ connect_menu_item self#main#newMenuItem newScript;
+ connect_key GdkKeysyms._period
+ (fun () ->
+ let buf = self#main#scriptTextView#buffer in
+ buf#insert ~iter:(buf#get_iter_at_mark `INSERT) ".\n";
+ advance ());
+ connect_key GdkKeysyms._Return
+ (fun () ->
+ let buf = self#main#scriptTextView#buffer in
+ buf#insert ~iter:(buf#get_iter_at_mark `INSERT) "\n";
+ advance ());
+ (* debug menu *)
+ self#main#debugMenu#misc#hide ();
+ (* status bar *)
+ self#main#hintLowImage#set_file "icons/matita-bulb-low.png";
+ self#main#hintMediumImage#set_file "icons/matita-bulb-medium.png";
+ self#main#hintHighImage#set_file "icons/matita-bulb-high.png";
+ (* focus *)
+ self#main#scriptTextView#misc#grab_focus ()
+
+ method console = console
+
+ method about = about
+ method fileSel = fileSel
+ method main = main
+
+ method newBrowserWin () =
+ let win = new browserWin () in
+ win#check_widgets ();
+ win
+
+ method newUriDialog () =
+ let dialog = new uriChoiceDialog () in
+ dialog#check_widgets ();
+ dialog
+
+ method newInterpDialog () =
+ let dialog = new interpChoiceDialog () in
+ dialog#check_widgets ();
+ dialog
+
+ method newConfirmationDialog () =
+ let dialog = new confirmationDialog () in
+ dialog#check_widgets ();
+ dialog
+
+ method newEmptyDialog () =
+ let dialog = new emptyDialog () in
+ dialog#check_widgets ();
+ dialog
+
+ method private addKeyBinding key callback =
+ List.iter (fun evbox -> add_key_binding key callback evbox)
+ keyBindingBoxes
+
+ method setQuitCallback callback =
+ ignore (main#toplevel#connect#destroy callback);
+ ignore (main#quitMenuItem#connect#activate callback);
+ self#addKeyBinding GdkKeysyms._q callback
+
+ method chooseFile ?(ok_not_exists = false) () =
+ _ok_not_exists <- ok_not_exists;
+ fileSel#fileSelectionWin#show ();
+ GtkThread.main ();
+ chosen_file
+
+ method askText ?(title = "") ?(msg = "") () =
+ let dialog = new textDialog () in
+ dialog#textDialog#set_title title;
+ dialog#textDialogLabel#set_label msg;
+ let text = ref None in
+ let return v =
+ text := v;
+ dialog#textDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
+ connect_button dialog#textDialogCancelButton (fun _ -> return None);
+ connect_button dialog#textDialogOkButton (fun _ ->
+ let text = dialog#textDialogTextView#buffer#get_text () in
+ return (Some text));
+ dialog#textDialog#show ();
+ GtkThread.main ();
+ !text
+
+ end
+
+let gui () =
+ let g = new gui () in
+ gui_instance := Some g;
+ g
+
+let instance = singleton gui
+
+let non p x = not (p x)
+
+let is_var_uri s =
+ try
+ String.sub s (String.length s - 4) 4 = ".var"
+ with Invalid_argument _ -> false
+
+let interactive_uri_choice
+ ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
+ ?(msg = "") ?(nonvars_button = false) ()
+ ~id uris
+=
+ let gui = instance () in
+ let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in
+ if (selection_mode <> `SINGLE) &&
+ (Helm_registry.get_bool "matita.auto_disambiguation")
+ then
+ Lazy.force nonvars_uris
+ else begin
+ let dialog = gui#newUriDialog () in
+ dialog#uriChoiceTreeView#selection#set_mode
+ (selection_mode :> Gtk.Tags.selection_mode);
+ let model = new stringListModel dialog#uriChoiceTreeView in
+ let choices = ref None in
+ let nonvars = ref false in
+ dialog#uriChoiceDialog#set_title title;
+ dialog#uriChoiceLabel#set_text msg;
+ List.iter model#easy_append uris;
+ dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
+ let return v =
+ choices := v;
+ dialog#uriChoiceDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
+ connect_button dialog#uriChoiceConstantsButton (fun _ ->
+ return (Some (Lazy.force nonvars_uris)));
+ connect_button dialog#uriChoiceAutoButton (fun _ ->
+ Helm_registry.set_bool "matita.auto_disambiguation" true;
+ return (Some (Lazy.force nonvars_uris)));
+ connect_button dialog#uriChoiceSelectedButton (fun _ ->
+ match model#easy_selection () with
+ | [] -> ()
+ | uris -> return (Some uris));
+ connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+ dialog#uriChoiceDialog#show ();
+ GtkThread.main ();
+ (match !choices with
+ | None -> raise MatitaTypes.Cancel
+ | Some uris -> uris)
+ end
+
+class interpModel =
+ let cols = new GTree.column_list in
+ let id_col = cols#add Gobject.Data.string in
+ let dsc_col = cols#add Gobject.Data.string in
+ let interp_no_col = cols#add Gobject.Data.int in
+ let tree_store = GTree.tree_store cols in
+ let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
+ let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
+ let id_view_col = GTree.view_column ~renderer:id_renderer () in
+ let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
+ fun tree_view choices ->
+ object
+ initializer
+ tree_view#set_model (Some (tree_store :> GTree.model));
+ ignore (tree_view#append_column id_view_col);
+ ignore (tree_view#append_column dsc_view_col);
+ let name_of_interp =
+ (* try to find a reasonable name for an interpretation *)
+ let idx = ref 0 in
+ fun interp ->
+ try
+ List.assoc "0" interp
+ with Not_found ->
+ incr idx; string_of_int !idx
+ in
+ tree_store#clear ();
+ let idx = ref ~-1 in
+ List.iter
+ (fun interp ->
+ incr idx;
+ let interp_row = tree_store#append () in
+ tree_store#set ~row:interp_row ~column:id_col
+ (name_of_interp interp);
+ tree_store#set ~row:interp_row ~column:interp_no_col !idx;
+ List.iter
+ (fun (id, dsc) ->
+ let row = tree_store#append ~parent:interp_row () in
+ tree_store#set ~row ~column:id_col id;
+ tree_store#set ~row ~column:dsc_col dsc;
+ tree_store#set ~row ~column:interp_no_col !idx)
+ interp)
+ choices
+
+ method get_interp_no tree_path =
+ let iter = tree_store#get_iter tree_path in
+ tree_store#get ~row:iter ~column:interp_no_col
+ end
+
+let interactive_interp_choice () choices =
+ let gui = instance () in
+ assert (choices <> []);
+ let dialog = gui#newInterpDialog () in
+ let model = new interpModel dialog#interpChoiceTreeView choices in
+ let interp_len = List.length (List.hd choices) in
+ dialog#interpChoiceDialog#set_title "Interpretation choice";
+ dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:";
+ let interp_no = ref None in
+ let return _ =
+ dialog#interpChoiceDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ let fail _ = interp_no := None; return () in
+ ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
+ connect_button dialog#interpChoiceOkButton (fun _ ->
+ match !interp_no with None -> () | Some _ -> return ());
+ connect_button dialog#interpChoiceCancelButton fail;
+ ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
+ interp_no := Some (model#get_interp_no path);
+ return ()));
+ let selection = dialog#interpChoiceTreeView#selection in
+ ignore (selection#connect#changed (fun _ ->
+ match selection#get_selected_rows with
+ | [path] ->
+ MatitaLog.debug (sprintf "selection: %d" (model#get_interp_no path));
+ interp_no := Some (model#get_interp_no path)
+ | _ -> assert false));
+ dialog#interpChoiceDialog#show ();
+ GtkThread.main ();
+ (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+class type console =
+object
+ method message: string -> unit
+ method error: string -> unit
+ method warning: string -> unit
+ method debug: string -> unit
+ method clear: unit -> unit
+
+ method log_callback: MatitaLog.log_callback
+end
+
+ (** @param fname name of the Glade file describing the GUI *)
+class type gui =
+object
+
+ method setQuitCallback : (unit -> unit) -> unit
+
+ (** {2 Access to singleton instances of lower-level GTK widgets} *)
+
+ method about : MatitaGeneratedGui.aboutWin
+ method fileSel : MatitaGeneratedGui.fileSelectionWin
+ method main : MatitaGeneratedGui.mainWin
+(* method toolbar : MatitaGeneratedGui.toolBarWin *)
+
+ method console: console
+
+ (** {2 Dialogs instantiation}
+ * methods below create a new window on each invocation. You should
+ * remember to destroy windows after use *)
+
+ method newBrowserWin: unit -> MatitaGeneratedGui.browserWin
+ method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+ method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog
+ method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
+ method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
+
+ (** {2 Utility methods} *)
+
+ (** ask the used to choose a file with the file chooser
+ * @param ok_not_exists if set to true returns also non existent files
+ * (useful for save). Defaults to false *)
+ method chooseFile: ?ok_not_exists:bool -> unit -> string option
+
+ (** prompt the user for a (multiline) text entry *)
+ method askText: ?title:string -> ?msg:string -> unit -> string option
+
+end
+
+ (** singleton instance of the gui *)
+val instance: unit -> gui
+
+ (** {2 Disambiguation callbacks}
+ * Use singleton gui instance. *)
+
+ (** @param selection_mode selection mode in uri list, default to `MULTIPLE
+ * @param title window title, defaults to ""
+ * @param msg message for the user, defaults to ""
+ * @param nonvars_button enable button to exclude vars?, defaults to false
+ * @raise MatitaTypes.Cancel *)
+val interactive_uri_choice:
+ ?selection_mode:([`SINGLE|`MULTIPLE]) -> ?title:string ->
+ ?msg:string -> ?nonvars_button:bool -> unit ->
+ MatitaDisambiguator.choose_uris_callback
+
+ (** @raise MatitaTypes.Cancel *)
+val interactive_interp_choice:
+ unit ->
+ MatitaDisambiguator.choose_interp_callback
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+type log_tag = [ `Debug | `Error | `Message | `Warning ]
+type log_callback = log_tag -> string -> unit
+
+let default_callback tag s =
+ let prefix =
+ match tag with
+ | `Message -> "Info: "
+ | `Warning -> "Warning: "
+ | `Error -> "Error: "
+ | `Debug -> "Debug: "
+ in
+ print_endline (prefix ^ s);
+ flush stdout
+
+let callback = ref default_callback
+
+let set_log_callback f = callback := f
+
+let message s = !callback `Message s
+let warn s = !callback `Warning s
+let error s = !callback `Error s
+let debug s = !callback `Debug s
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+type log_tag = [ `Debug | `Error | `Message | `Warning ]
+type log_callback = log_tag -> string -> unit
+
+val set_log_callback: log_callback -> unit
+
+val message : string -> unit
+val warn : string -> unit
+val error : string -> unit
+val debug : string -> unit
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+open Printf
+
+open MatitaTypes
+
+let list_map_fail f =
+ let rec aux = function
+ | [] -> []
+ | he::tl ->
+ try
+ let he' = f he in
+ he'::(aux tl)
+ with Exit ->
+ (aux tl)
+ in
+ aux
+
+(** inherit from this class if you want to access current script *)
+class scriptAccessor =
+object (self)
+ method private script = MatitaScript.instance ()
+end
+
+class clickableMathView obj =
+ let href = Gdome.domString "href" in
+ let xref = Gdome.domString "xref" in
+ object (self)
+ inherit GMathViewAux.multi_selection_math_view obj
+
+ val mutable href_callback: (string -> unit) option = None
+ method set_href_callback f = href_callback <- f
+
+ initializer
+ ignore (self#connect#selection_changed self#choose_selection);
+ ignore (self#connect#click (fun (gdome_elt, _, _, _) ->
+ match gdome_elt with
+ | Some elt (* element is an hyperlink, use href_callback on it *)
+ when elt#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href ->
+ (match href_callback with
+ | None -> ()
+ | Some f ->
+ let uri =
+ elt#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href
+ in
+ f (uri#to_string))
+ | Some elt -> ignore (self#action_toggle elt)
+ | None -> ()))
+ method private choose_selection gdome_elt =
+ let rec aux elt =
+ if elt#hasAttributeNS ~namespaceURI:Misc.helm_ns ~localName:xref then
+ self#set_selection (Some elt)
+ else
+ try
+ (match elt#get_parentNode with
+ | None -> assert false
+ | Some p -> aux (new Gdome.element_of_node p))
+ with GdomeInit.DOMCastException _ -> ()
+(* debug_print "trying to select above the document root" *)
+ in
+ match gdome_elt with
+ | Some elt -> aux elt
+ | None -> self#set_selection None
+ end
+
+let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity =
+ GtkBase.Widget.size_params
+ ~cont:(OgtkMathViewProps.pack_return (fun p ->
+ OgtkMathViewProps.set_params
+ (new clickableMathView (GtkMathViewProps.MathView_GMetaDOM.create p))
+ ~font_size:None ~log_verbosity:None))
+ []
+
+class sequentViewer obj =
+ object(self)
+
+ inherit clickableMathView obj
+
+ val mutable current_infos = None
+
+ method get_selected_terms =
+ let selections = self#get_selections in
+ list_map_fail
+ (fun node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ ~namespaceURI:Misc.helm_ns
+ ~localName:(Gdome.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ match current_infos with
+ | Some (ids_to_terms,_,_) ->
+ (try Hashtbl.find ids_to_terms xpath with _ -> raise Exit)
+ | None -> assert false) (* "ERROR: No current term!!!" *)
+ selections
+
+ method get_selected_hypotheses =
+ let selections = self#get_selections in
+ list_map_fail
+ (fun node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ ~namespaceURI:Misc.helm_ns
+ ~localName:(Gdome.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ match current_infos with
+ | Some (_,_,ids_to_hypotheses) ->
+ (try Hashtbl.find ids_to_hypotheses xpath with _ -> raise Exit)
+ | None -> assert false) (* "ERROR: No current term!!!" *)
+ selections
+
+ method load_sequent metasenv metano =
+ let sequent = CicUtil.lookup_meta metano metasenv in
+ let (mathml,(_,(ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_))) =
+ ApplyTransformation.mml_of_cic_sequent metasenv sequent
+ in
+ current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
+(*
+ debug_print "load_sequent: dumping MathML to ./prova";
+ ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ());
+*)
+ self#load_root ~root:mathml#get_documentElement
+ end
+
+class sequentsViewer ~(notebook:GPack.notebook)
+ ~(sequentViewer:sequentViewer) ()
+=
+ object (self)
+ inherit scriptAccessor
+
+ val mutable pages = 0
+ val mutable switch_page_callback = None
+ val mutable page2goal = [] (* associative list: page no -> goal no *)
+ val mutable goal2page = [] (* the other way round *)
+ val mutable goal2win = [] (* associative list: goal no -> scrolled win *)
+ val mutable _metasenv = []
+ val mutable scrolledWin: GBin.scrolled_window option = None
+ (* scrolled window to which the sequentViewer is currently attached *)
+
+ method private tab_label metano =
+ (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
+
+ method reset =
+ (match scrolledWin with
+ | Some w ->
+ (* removing page from the notebook will destroy all contained widget,
+ * we do not want the sequentViewer to be destroyed as well *)
+ w#remove sequentViewer#coerce;
+ scrolledWin <- None
+ | None -> ());
+ for i = 1 to pages do notebook#remove_page 0 done;
+ pages <- 0;
+ page2goal <- [];
+ goal2page <- [];
+ goal2win <- [];
+ _metasenv <- [];
+ self#script#setGoal ~-1;
+ (match switch_page_callback with
+ | Some id ->
+ GtkSignal.disconnect notebook#as_widget id;
+ switch_page_callback <- None
+ | None -> ())
+
+ method load_sequents (status: ProofEngineTypes.status) =
+ let ((_, metasenv, _, _), goal) = status in
+ let sequents_no = List.length metasenv in
+ _metasenv <- metasenv;
+ pages <- sequents_no;
+ self#script#setGoal goal;
+ let win metano =
+ let w =
+ GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
+ ~shadow_type:`IN ~show:true ()
+ in
+ let reparent () =
+ scrolledWin <- Some w;
+ match sequentViewer#misc#parent with
+ | None -> w#add sequentViewer#coerce
+ | Some _ -> sequentViewer#misc#reparent w#coerce
+ in
+ goal2win <- (metano, reparent) :: goal2win;
+ w#coerce
+ in
+ let page = ref 0 in
+ List.iter
+ (fun (metano, _, _) ->
+ page2goal <- (!page, metano) :: page2goal;
+ goal2page <- (metano, !page) :: goal2page;
+ incr page;
+ notebook#append_page ~tab_label:(self#tab_label metano) (win metano))
+ metasenv;
+ switch_page_callback <-
+ Some (notebook#connect#switch_page ~callback:(fun page ->
+ let goal =
+ try
+ List.assoc page page2goal
+ with Not_found -> assert false
+ in
+ self#script#setGoal goal;
+ self#render_page ~page ~goal))
+
+ method private render_page ~page ~goal =
+ sequentViewer#load_sequent _metasenv goal;
+ try
+ List.assoc goal goal2win ();
+ sequentViewer#set_selection None
+ with Not_found -> assert false
+
+ method goto_sequent goal =
+ let page =
+ try
+ List.assoc goal goal2page
+ with Not_found -> assert false
+ in
+ notebook#goto_page page;
+ self#render_page page goal
+
+ end
+
+ (** constructors *)
+
+type 'widget constructor =
+ ?hadjustment:GData.adjustment ->
+ ?vadjustment:GData.adjustment ->
+ ?font_size:int ->
+ ?log_verbosity:int ->
+ ?width:int ->
+ ?height:int ->
+ ?packing:(GObj.widget -> unit) ->
+ ?show:bool ->
+ unit ->
+ 'widget
+
+let sequentViewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
+ GtkBase.Widget.size_params
+ ~cont:(OgtkMathViewProps.pack_return (fun p ->
+ OgtkMathViewProps.set_params
+ (new sequentViewer (GtkMathViewProps.MathView_GMetaDOM.create p))
+ ~font_size ~log_verbosity))
+ []
+
+let blank_uri = BuildTimeConf.blank_uri
+let current_proof_uri = BuildTimeConf.current_proof_uri
+
+type term_source =
+ [ `Ast of DisambiguateTypes.term
+ | `Cic of Cic.term * Cic.metasenv
+ | `String of string
+ ]
+
+exception Browser_failure of string
+
+let cicBrowsers = ref []
+
+class type cicBrowser =
+object
+ method loadUri: string -> unit
+ method loadTerm: term_source -> unit
+end
+
+class cicBrowser_impl ~(history:string MatitaMisc.history) () =
+ let term_RE = Pcre.regexp "^term:(.*)" in
+ let trailing_slash_RE = Pcre.regexp "/$" in
+ let gui = MatitaGui.instance () in
+ let win = gui#newBrowserWin () in
+ let toplevel = win#toplevel in
+ let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in
+ let fail msg =
+ ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ())
+ ~title:"Cic browser" ~msg ~cancel:false ());
+ in
+ let handle_error f =
+ try
+ f ()
+ with exn ->
+ fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn))
+ in
+ let handle_error' f = fun () -> handle_error f in (* used in callbacks *)
+ object (self)
+ inherit scriptAccessor
+
+ initializer
+ ignore (win#browserUri#connect#activate (handle_error' (fun () ->
+ self#_loadUri win#browserUri#text)));
+ ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
+ self#_loadUri current_proof_uri)));
+ ignore (win#browserRefreshButton#connect#clicked
+ (handle_error' self#refresh));
+ ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
+ ignore (win#browserForwardButton#connect#clicked
+ (handle_error' self#forward));
+ ignore (win#toplevel#event#connect#delete (fun _ ->
+ let my_id = Oo.id self in
+ cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
+ if !cicBrowsers = [] &&
+ Helm_registry.get "matita.mode" = "cicbrowser"
+ then
+ GMain.quit ();
+ false));
+ mathView#set_href_callback (Some (fun uri ->
+ handle_error (fun () -> self#_loadUri uri)));
+ self#_loadUri ~add_to_history:false blank_uri;
+ toplevel#show ();
+
+ val mutable current_uri = ""
+ val mutable current_infos = None
+ val mutable current_mathml = None
+
+ method private back () =
+ try
+ self#_loadUri ~add_to_history:false history#previous
+ with MatitaMisc.History_failure -> ()
+
+ method private forward () =
+ try
+ self#_loadUri ~add_to_history:false history#next
+ with MatitaMisc.History_failure -> ()
+
+ (* loads a uri which can be a cic uri or an about:* uri
+ * @param uri string *)
+ method private _loadUri ?(add_to_history = true) uri =
+ try
+ if current_uri <> uri || uri = current_proof_uri then begin
+ (match uri with
+ | uri when uri = blank_uri -> self#blank ()
+ | uri when uri = current_proof_uri -> self#home ()
+ | uri when Pcre.pmatch ~rex:term_RE uri ->
+ self#loadTerm (`String (Pcre.extract ~rex:term_RE uri).(1))
+ | uri when Pcre.pmatch ~rex:trailing_slash_RE uri -> self#loadDir uri
+ | _ -> self#loadUriManagerUri (UriManager.uri_of_string uri));
+ self#setUri uri;
+ if add_to_history then history#add uri
+ end
+ with
+ | UriManager.IllFormedUri _ -> fail (sprintf "invalid uri: %s" uri)
+ | CicEnvironment.Object_not_found _ ->
+ fail (sprintf "object not found: %s" uri)
+ | Browser_failure msg -> fail msg
+
+ method loadUri uri =
+ handle_error (fun () -> self#_loadUri ~add_to_history:true uri)
+
+ method private blank () =
+ mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement
+
+ method private home () =
+ if self#script#onGoingProof () then
+ let ((uri, metasenv, bo, ty), _) = self#script#proofStatus in
+ let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in
+ let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+ self#loadObj obj
+ else
+ self#blank ()
+
+ (** loads a cic uri from the environment
+ * @param uri UriManager.uri *)
+ method private loadUriManagerUri uri =
+ let uri = UriManager.strip_xpointer uri in
+ let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ self#loadObj obj
+
+ method private loadDir dir =
+ let mathml = MatitaMisc.empty_boxml () in
+ let content = Http_getter.ls dir in
+ let root = mathml#get_documentElement in
+ let new_box_elt name =
+ mathml#createElementNS ~namespaceURI:(Some Misc.boxml_ns)
+ ~qualifiedName:(Gdome.domString ("b:" ^ name))
+ in
+ let new_text content = mathml#createTextNode (Gdome.domString content) in
+ let b_v = new_box_elt "v" in
+ List.iter
+ (fun item ->
+ let b_text = new_box_elt "text" in
+ let uri, elt =
+ match item with
+ | Http_getter_types.Ls_section subdir ->
+ (dir ^ subdir ^ "/"), (new_text (subdir ^ "/"))
+ | Http_getter_types.Ls_object obj ->
+ (dir ^ obj.Http_getter_types.uri),
+ (new_text obj.Http_getter_types.uri)
+ in
+ b_text#setAttributeNS ~namespaceURI:(Some Misc.xlink_ns)
+ ~qualifiedName:(Gdome.domString "xlink:href")
+ ~value:(Gdome.domString uri);
+ ignore (b_v#appendChild ~newChild:(b_text :> Gdome.node));
+ ignore (b_text#appendChild ~newChild:(elt :> Gdome.node)))
+ content;
+ ignore (root#appendChild ~newChild:(b_v :> Gdome.node));
+(* Misc.domImpl#saveDocumentToFile ~doc:mathml ~name:"pippo" (); *)
+ mathView#load_root ~root:root
+
+ method private setUri uri =
+ win#browserUri#set_text uri;
+ current_uri <- uri
+
+ method private loadObj obj =
+ let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *)
+ let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures,
+ ids_to_hypotheses,_,_))) =
+ ApplyTransformation.mml_of_cic_object obj
+ in
+ current_infos <- Some (ids_to_terms, ids_to_father_ids,
+ ids_to_conjectures, ids_to_hypotheses);
+ match current_mathml with
+ | Some current_mathml when use_diff ->
+ mathView#freeze;
+ XmlDiff.update_dom ~from:current_mathml mathml;
+ mathView#thaw
+ | _ ->
+ mathView#load_root ~root:mathml#get_documentElement;
+ current_mathml <- Some mathml
+
+ method private _loadTerm s = failwith "not implemented _loadTerm"
+(* TODO self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s)) *)
+
+ method private _loadTermAst ast = failwith "not implemented _loadTermAst"
+(* TODO
+ let (_, metasenv, term, _) =
+ MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
+ in
+ self#_loadTermCic term metasenv
+*)
+
+ method private _loadTermCic term metasenv =
+ let context = self#script#proofContext in
+ let dummyno = CicMkImplicit.new_meta metasenv [] in
+ let sequent = (dummyno, context, term) in
+ mathView#load_sequent (sequent :: metasenv) dummyno
+
+ method loadTerm (src:term_source) =
+ handle_error (fun () ->
+ (match src with
+ | `Ast ast -> self#_loadTermAst ast
+ | `Cic (cic, metasenv) -> self#_loadTermCic cic metasenv
+ | `String s -> self#_loadTerm s);
+ self#setUri "check")
+
+ (** {2 methods used by constructor only} *)
+
+ method win = win
+ method history = history
+ method currentUri = current_uri
+ method refresh () =
+ if current_uri = current_proof_uri then
+ self#_loadUri ~add_to_history:false current_proof_uri
+
+ end
+
+let sequentsViewer ~(notebook:GPack.notebook)
+ ~(sequentViewer:sequentViewer) ()
+=
+ new sequentsViewer ~notebook ~sequentViewer ()
+
+let cicBrowser () =
+ let size = BuildTimeConf.browser_history_size in
+ let rec aux history =
+ let browser = new cicBrowser_impl ~history () in
+ let win = browser#win in
+ ignore (win#browserNewButton#connect#clicked (fun () ->
+ let history =
+ new MatitaMisc.browser_history ~memento:history#save size ""
+ in
+ let newBrowser = aux history in
+ newBrowser#loadUri browser#currentUri));
+(*
+ (* attempt (failed) to close windows on CTRL-W ... *)
+ MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL]
+ GdkKeysyms._W (fun () -> win#toplevel#destroy ());
+*)
+ cicBrowsers := browser :: !cicBrowsers;
+ (browser :> cicBrowser)
+ in
+ let history = new MatitaMisc.browser_history size blank_uri in
+ aux history
+
+let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers
+
+let default_sequentViewer () = sequentViewer ~show:true ()
+let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer
+
+let default_sequentsViewer () =
+ let gui = MatitaGui.instance () in
+ let sequentViewer = sequentViewer_instance () in
+ sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer ()
+let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+ (** multi selection gtkMathView which handle mactions and hyperlinks. Mactions
+ * are handled internally. Hyperlinks are handled by calling an user provided
+ * callback *)
+class type clickableMathView =
+ object
+ inherit GMathViewAux.multi_selection_math_view
+
+ (** set hyperlink callback. None disable hyperlink handling *)
+ method set_href_callback: (string -> unit) option -> unit
+ end
+
+class type sequentViewer =
+ object
+ inherit clickableMathView
+
+ (** @return the list of selected terms. Selections which are not terms are
+ * ignored *)
+ method get_selected_terms: Cic.term list
+
+ (** @return the list of selected hypothese. Selections which are not
+ * hypotheses are ignored *)
+ method get_selected_hypotheses: Cic.hypothesis list
+
+ (** load a sequent and render it into parent widget *)
+ method load_sequent: Cic.metasenv -> int -> unit
+ end
+
+class type sequentsViewer =
+ object
+ method reset: unit
+ method load_sequents: ProofEngineTypes.status -> unit
+ method goto_sequent: int -> unit (* to be called _after_ load_sequents *)
+ end
+
+exception Browser_failure of string
+
+type term_source =
+ [ `Ast of DisambiguateTypes.term
+ | `Cic of Cic.term * Cic.metasenv
+ | `String of string
+ ]
+
+class type cicBrowser =
+object
+ method loadUri: string -> unit
+ method loadTerm: term_source -> unit
+end
+
+(** {2 Constructors} *)
+
+ (** meta constructor *)
+type 'widget constructor =
+ ?hadjustment:GData.adjustment ->
+ ?vadjustment:GData.adjustment ->
+ ?font_size:int ->
+ ?log_verbosity:int ->
+ ?width:int ->
+ ?height:int ->
+ ?packing:(GObj.widget -> unit) ->
+ ?show:bool ->
+ unit ->
+ 'widget
+
+val clickableMathView: clickableMathView constructor
+
+val sequentViewer: sequentViewer constructor
+
+val sequentsViewer:
+ notebook:GPack.notebook ->
+ sequentViewer:sequentViewer ->
+ unit ->
+ sequentsViewer
+
+val cicBrowser: unit -> cicBrowser
+
+val refresh_all_browsers: unit -> unit
+
+(** {2 singleton instances} *)
+
+val sequentViewer_instance: unit -> sequentViewer
+val sequentsViewer_instance: unit -> sequentsViewer
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+open MatitaTypes
+
+let is_dir fname =
+ try
+ (Unix.stat fname).Unix.st_kind = Unix.S_DIR
+ with Unix.Unix_error _ -> false
+
+let is_regular fname =
+ try
+ (Unix.stat fname).Unix.st_kind = Unix.S_REG
+ with Unix.Unix_error _ -> false
+
+let input_file fname =
+ let size = (Unix.stat fname).Unix.st_size in
+ let buf = Buffer.create size in
+ let ic = open_in fname in
+ Buffer.add_channel buf ic size;
+ close_in ic;
+ Buffer.contents buf
+
+let is_proof_script fname = true (** TODO Zack *)
+let is_proof_object fname = true (** TODO Zack *)
+
+let append_phrase_sep s =
+ if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then
+ s ^ BuildTimeConf.phrase_sep
+ else
+ s
+
+let strip_trailing_blanks =
+ let rex = Pcre.regexp "\\s*$" in
+ fun s -> Pcre.replace ~rex s
+
+let empty_mathml () =
+ Misc.domImpl#createDocument ~namespaceURI:(Some Misc.mathml_ns)
+ ~qualifiedName:(Gdome.domString "math") ~doctype:None
+
+let empty_boxml () =
+ Misc.domImpl#createDocument ~namespaceURI:(Some Misc.boxml_ns)
+ ~qualifiedName:(Gdome.domString "box") ~doctype:None
+
+exception History_failure
+
+type 'a memento = 'a array * int * int * int (* data, hd, tl, cur *)
+
+class type ['a] history =
+ object
+ method add : 'a -> unit
+ method next : 'a
+ method previous : 'a
+ method load: 'a memento -> unit
+ method save: 'a memento
+ end
+
+class shell_history size =
+ let size = size + 1 in
+ let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in
+ let incr x = (x + 1) mod size in
+ object (self)
+ val data = Array.create size ""
+ val mutable hd = 0 (* insertion point *)
+ val mutable tl = -1 (* oldest inserted item *)
+ val mutable cur = -1 (* current item for the history *)
+ method add s =
+ data.(hd) <- s;
+ if tl = -1 then tl <- hd;
+ hd <- incr hd;
+ if hd = tl then tl <- incr tl;
+ cur <- hd
+ method previous =
+ if cur = tl then raise History_failure;
+ cur <- decr cur;
+ data.(cur)
+ method next =
+ if cur = hd then raise History_failure;
+ cur <- incr cur;
+ if cur = hd then "" else data.(cur)
+ method load (data', hd', tl', cur') =
+ assert (Array.length data = Array.length data');
+ hd <- hd'; tl <- tl'; cur <- cur';
+ Array.blit data' 0 data 0 (Array.length data')
+ method save = (Array.copy data, hd, tl, cur)
+ end
+
+class ['a] browser_history ?memento size init =
+ object (self)
+ initializer match memento with Some m -> self#load m | _ -> ()
+ val data = Array.create size init
+ val mutable hd = 0
+ val mutable tl = 0
+ val mutable cur = 0
+ method previous =
+ if cur = tl then raise History_failure;
+ cur <- cur - 1;
+ if cur = ~-1 then cur <- size - 1;
+ data.(cur)
+ method next =
+ if cur = hd then raise History_failure;
+ cur <- cur + 1;
+ if cur = size then cur <- 0;
+ data.(cur)
+ method add (e:'a) =
+ cur <- cur + 1;
+ if cur = size then cur <- 0;
+ if cur = tl then tl <- tl + 1;
+ if tl = size then tl <- 0;
+ hd <- cur;
+ data.(cur) <- e
+ method load (data', hd', tl', cur') =
+ assert (Array.length data = Array.length data');
+ hd <- hd'; tl <- tl'; cur <- cur';
+ Array.blit data' 0 data 0 (Array.length data')
+ method save = (Array.copy data, hd, tl, cur)
+ end
+
+let singleton f =
+ let instance = lazy (f ()) in
+ fun () -> Lazy.force instance
+
+let mkdir d =
+ let errmsg = sprintf "Unable to create directory \"%s\"" d in
+ try
+ (match Unix.system ("mkdir -p " ^ d) with
+ | Unix.WEXITED 0 -> ()
+ | _ -> failwith errmsg)
+ with Unix.Unix_error _ -> failwith errmsg
+
+let get_proof_status status =
+ match status.proof_status with
+ | Incomplete_proof s -> s
+ | _ -> statement_error "no ongoing proof"
+
+let get_proof_metasenv status =
+ match status.proof_status with
+ | No_proof -> []
+ | Incomplete_proof ((_, metasenv, _, _), _) -> metasenv
+ | Proof (_, metasenv, _, _) -> metasenv
+ | Intermediate m -> m
+
+let get_proof_context status =
+ match status.proof_status with
+ | Incomplete_proof ((_, metasenv, _, _), goal) ->
+ let (_, context, _) = CicUtil.lookup_meta goal metasenv in
+ context
+ | _ -> []
+
+let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
+
+let unopt = function None -> failwith "unopt: None" | Some v -> v
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val is_dir: string -> bool (** @return true if file is a directory *)
+val is_regular: string -> bool (** @return true if file is a regular file *)
+
+val input_file: string -> string (** read all the contents of file to string *)
+
+ (** @return true if file is a (textual) proof script *)
+val is_proof_script: string -> bool
+
+ (** @return true if file is a (binary) proof object *)
+val is_proof_object: string -> bool
+
+ (** given a phrase, if it doesn't end with BuildTimeConf.phrase_sep, append
+ * it *)
+val append_phrase_sep: string -> string
+
+val strip_trailing_blanks: string -> string
+
+ (** @raise Failure *)
+val unopt: 'a option -> 'a
+
+ (** Gdome.element of a MathML document whose rendering should be blank. Used
+ * by cicBrowser to render "about:blank" document *)
+val empty_mathml: unit -> Gdome.document
+val empty_boxml: unit -> Gdome.document
+
+exception History_failure
+
+type 'a memento
+
+class type ['a] history =
+ object ('b)
+ method add : 'a -> unit
+ method next : 'a (** @raise History_failure *)
+ method previous : 'a (** @raise History_failure *)
+ method load: 'a memento -> unit
+ method save: 'a memento
+ end
+
+ (** shell like history: new items added at the end of the history
+ * @param size maximum history size *)
+class shell_history : int -> [string] history
+
+ (** browser like history: new items added at the current point of the history
+ * @param size maximum history size
+ * @param first element in history (this history is never empty) *)
+class ['a] browser_history: ?memento:'a memento -> int -> 'a -> ['a] history
+
+ (** create a singleton from a given function. Given function is invoked the
+ * first time it gets called. Next invocation will return first value *)
+val singleton: (unit -> 'a) -> (unit -> 'a)
+
+ (** create a directory, building also parents if needed
+ * @raise Failure when unable to create some directory *)
+val mkdir: string -> unit
+
+val qualify: MatitaTypes.status -> string -> string
+
+val get_proof_status: MatitaTypes.status -> ProofEngineTypes.status
+val get_proof_metasenv: MatitaTypes.status -> Cic.metasenv
+val get_proof_context: MatitaTypes.status -> Cic.context
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+open MatitaTypes
+
+ (** raised when one of the script margins (top or bottom) is reached *)
+exception Margin
+
+let safe_substring s i j =
+ try String.sub s i j with Invalid_argument _ -> assert false
+
+let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*"
+let blanks_RE = Pcre.regexp "^\\s*$"
+
+let first_line s =
+ let s = Pcre.replace ~rex:heading_nl_RE s in
+ try
+ let nl_pos = String.index s '\n' in
+ String.sub s 0 nl_pos
+ with Not_found -> s
+
+let prepend_text header base =
+ if Pcre.pmatch ~rex:heading_nl_RE base then
+ sprintf "\n%s%s" header base
+ else
+ sprintf "%s\n%s" header base
+
+ (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
+let goal_ast n =
+ let module A = TacticAst in
+ let loc = CicAst.dummy_floc in
+ A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n)))
+
+let eval_statement status user_goal s =
+ let st = CicTextualParser2.parse_statement (Stream.of_string s) in
+ match st with
+ | TacticAst.Command (loc, _) | TacticAst.Tactical (loc, _) ->
+ let parsed_text_length = snd (CicAst.loc_of_floc loc) in
+ let parsed_text = safe_substring s 0 parsed_text_length in
+ let goal_changed = ref false in
+ let status =
+ match status.proof_status with
+ | Incomplete_proof (_, goal) when goal <> user_goal ->
+ goal_changed := true;
+ MatitaEngine.eval_ast status (goal_ast user_goal)
+ | _ -> status
+ in
+ let new_status = MatitaEngine.eval_ast status st in
+ let new_aliases =
+ match st with
+ | TacticAst.Command (_, TacticAst.Alias _) ->
+ DisambiguateTypes.Environment.empty
+ | _ -> MatitaSync.alias_diff ~from:status new_status
+ in
+ let new_text =
+ if DisambiguateTypes.Environment.is_empty new_aliases then
+ parsed_text
+ else
+ prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases)
+ parsed_text
+ in
+ let new_text =
+ if !goal_changed then
+ prepend_text
+ (TacticAstPp.pp_tactic (TacticAst.Goal (loc, user_goal))(* ^ "\n"*))
+ new_text
+ else
+ new_text
+ in
+ [ new_status, new_text ], parsed_text_length
+ | TacticAst.Macro (loc, mac) ->
+ (match mac with (* TODO *)
+ | _ -> failwith "not implemented")
+
+class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) () =
+object (self)
+ initializer self#reset ()
+
+ val mutable statements = []; (** executed statements *)
+ val mutable history = [ init ];
+ (** list of states before having executed statements. Head element of this
+ * list is the current state, last element is the state at the beginning of
+ * the script.
+ * Invariant: this list length is 1 + length of statements *)
+
+ (** goal as seen by the user (i.e. metano corresponding to current tab) *)
+ val mutable userGoal = ~-1
+
+ (** text mark and tag representing locked part of a script *)
+ val locked_mark =
+ buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
+ val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
+
+ (* history can't be empty, the invariant above grant that it contains at
+ * least the init status *)
+ method status = match history with hd :: _ -> hd | _ -> assert false
+
+ method private _advance ?statement () =
+ let s = match statement with Some s -> s | None -> self#getFuture in
+ if Pcre.pmatch ~rex:blanks_RE s then raise Margin;
+ MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
+ let (entries, parsed_len) = eval_statement self#status userGoal s in
+ let (new_statuses, new_statements) = List.split entries in
+(*
+prerr_endline "evalStatement returned";
+List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements;
+*)
+ history <- List.rev new_statuses @ history;
+ statements <- List.rev new_statements @ statements;
+ let start = buffer#get_iter_at_mark (`MARK locked_mark) in
+ if statement = None then begin
+ let stop = start#copy#forward_chars parsed_len in
+ buffer#delete ~start ~stop
+ end;
+ let new_text = String.concat "" new_statements in
+ buffer#insert ~iter:start new_text;
+ self#moveMark (String.length new_text);
+
+ method private _retract () =
+ match statements, history with
+ | last_statement :: _, cur_status :: prev_status :: _ ->
+ MatitaSync.time_travel ~present:cur_status ~past:prev_status;
+ statements <- List.tl statements;
+ history <- List.tl history;
+ self#moveMark (- (String.length last_statement))
+ | _ -> raise Margin
+
+ method advance ?statement () =
+ try
+ self#_advance ?statement ()
+ with Margin -> ()
+
+ method retract () = try self#_retract () with Margin -> ()
+
+ method private getFuture =
+ buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
+ ~stop:buffer#end_iter ()
+
+ (** @param rel_offset relative offset from current position of locked_mark *)
+ method private moveMark rel_offset =
+ let mark = `MARK locked_mark in
+ buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
+ let current_mark_pos = buffer#get_iter_at_mark mark in
+ let new_mark_pos =
+ match rel_offset with
+ | 0 -> current_mark_pos
+ | n when n > 0 -> current_mark_pos#forward_chars n
+ | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n)
+ in
+ buffer#move_mark mark ~where:new_mark_pos;
+ buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
+ self#notify
+
+ val mutable observers = []
+
+ method addObserver (o: MatitaTypes.status -> unit) =
+ observers <- o :: observers
+
+ method private notify =
+ let status = self#status in
+ List.iter (fun o -> o status) observers
+
+ method loadFrom fname =
+ buffer#set_text (MatitaMisc.input_file fname);
+ self#goto_top
+
+ method saveTo fname =
+ let oc = open_out fname in
+ output_string oc (buffer#get_text ~start:buffer#start_iter
+ ~stop:buffer#end_iter ());
+ close_out oc
+
+ method private goto_top =
+ MatitaSync.time_travel ~present:self#status ~past:init;
+ statements <- [];
+ history <- [ init ];
+ userGoal <- ~-1;
+ self#notify;
+ buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
+ buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
+
+ method reset () =
+ self#goto_top;
+ buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
+
+ method goto (pos: [`Top | `Bottom | `Cursor]) () =
+ match pos with
+ | `Top -> self#goto_top
+ | `Bottom ->
+ (try while true do self#_advance () done with Margin -> ())
+ | `Cursor ->
+ let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
+ let cursor_iter () = buffer#get_iter_at_mark `INSERT in
+ let rec forward_until_cursor () = (* go forward until locked > cursor *)
+ self#_advance ();
+ if (locked_iter ())#compare (cursor_iter ()) < 0 then
+ forward_until_cursor ()
+ in
+ let rec back_until_cursor () = (* go backward until locked < cursor *)
+ self#_retract ();
+ if (locked_iter ())#compare (cursor_iter ()) > 0 then
+ back_until_cursor ()
+ in
+ let cmp = (locked_iter ())#compare (cursor_iter ()) in
+ (try
+ if cmp < 0 then (* locked < cursor *)
+ forward_until_cursor ()
+ else if cmp > 0 then (* locked > cursor *)
+ back_until_cursor ()
+ else (* cursor = locked *)
+ ()
+ with Margin -> ())
+
+ method onGoingProof () =
+ match self#status.proof_status with
+ | No_proof | Proof _ -> false
+ | Incomplete_proof _ -> true
+ | Intermediate _ -> assert false
+
+ method proofStatus = MatitaMisc.get_proof_status self#status
+ method proofMetasenv = MatitaMisc.get_proof_metasenv self#status
+ method proofContext = MatitaMisc.get_proof_context self#status
+ method setGoal n = userGoal <- n
+
+ (* debug *)
+ method dump () =
+ MatitaLog.debug "script status:";
+ MatitaLog.debug ("history size: " ^ string_of_int (List.length history));
+ MatitaLog.debug (sprintf "%d statements:" (List.length statements));
+ List.iter MatitaLog.debug statements;
+
+end
+
+let _script = ref None
+
+let script ~buffer ~init () =
+ let s = new script ~buffer ~init () in
+ _script := Some s;
+ s
+
+let instance () = match !_script with None -> assert false | Some s -> s
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+class type script =
+object
+
+ (** @return current status *)
+ method status: MatitaTypes.status
+
+ (** {2 Observers} *)
+
+ method addObserver : (MatitaTypes.status -> unit) -> unit
+
+ (** {2 History} *)
+
+ method advance : ?statement:string -> unit -> unit
+ method retract : unit -> unit
+ method goto: [`Top | `Bottom | `Cursor] -> unit -> unit
+ method reset: unit -> unit
+
+ (** {2 Load/save} *)
+
+ method loadFrom : string -> unit
+ method saveTo : string -> unit
+
+ (** {2 Current proof} (if any) *)
+
+ (** @return true if there is an ongoing proof, false otherise *)
+ method onGoingProof: unit -> bool
+
+ method proofStatus: ProofEngineTypes.status (** @raise Statement_error *)
+ method proofMetasenv: Cic.metasenv (** @raise Statement_error *)
+ method proofContext: Cic.context (** @raise Statement_error *)
+
+ method setGoal: int -> unit
+
+ (* debug *)
+ method dump : unit -> unit
+
+end
+
+val script: buffer:GText.buffer -> init:MatitaTypes.status -> unit -> script
+
+(* each time script above is called an internal ref is set, instance will return
+ * the value of this ref *)
+(* TODO Zack: orrible solution until we found a better one for having a single
+ * access point for the script *)
+val instance: unit -> script
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+open MatitaTypes
+
+let paths_and_uris_of_obj uri status =
+ let basedir = get_string_option status "basedir" in
+ let innertypesuri = UriManager.innertypesuri_of_uri uri in
+ let bodyuri = UriManager.bodyuri_of_uri uri in
+ let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
+ (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
+ let innertypespath = basedir ^ "/" ^ innertypesfilename in
+ let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
+ (UriManager.string_of_uri uri) ^ ".xml.gz" in
+ let xmlpath = basedir ^ "/" ^ xmlfilename in
+ let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
+ (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
+ let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in
+ xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri
+
+let save_object_to_disk status uri obj =
+ let ensure_path_exists path =
+ let dir = Filename.dirname path in
+ MatitaMisc.mkdir dir
+ in
+ (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
+ let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
+ Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
+ in
+ (* prepare XML *)
+ let xml, bodyxml =
+ Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
+ annobj
+ in
+ let xmlinnertypes =
+ Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+ ~ask_dtd_to_the_getter:false
+ in
+ let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri =
+ paths_and_uris_of_obj uri status
+ in
+ let path_scheme_of path = "file://" ^ path in
+ List.iter MatitaMisc.mkdir
+ (List.map Filename.dirname [innertypespath; xmlpath]);
+ (* now write to disk *)
+ ensure_path_exists innertypespath;
+ Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ;
+ ensure_path_exists xmlpath;
+ Xml.pp ~gzip:true xml (Some xmlpath) ;
+ (* now register to the getter *)
+ Http_getter.register' innertypesuri (path_scheme_of innertypespath);
+ Http_getter.register' uri (path_scheme_of xmlpath);
+ (* we return a list of uri,path we registered/created *)
+ (uri,xmlpath) :: (innertypesuri,innertypespath) ::
+ (* now the optional body, both write and register *)
+ (match bodyxml,bodyuri with
+ None,None -> []
+ | Some bodyxml,Some bodyuri->
+ ensure_path_exists xmlbodypath;
+ Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ;
+ Http_getter.register' bodyuri (path_scheme_of xmlbodypath);
+ [bodyuri,xmlbodypath]
+ | _-> assert false)
+
+let unregister_if_some = function
+ | Some u -> Http_getter.unregister' u | None -> ()
+
+let remove_object_from_disk uri path =
+ Sys.remove path;
+ Http_getter.unregister' uri
+
+let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status =
+ let dbd = MatitaDb.instance () in
+ let suri = UriManager.string_of_uri uri in
+ if CicEnvironment.in_library uri then
+ command_error (sprintf "%s constant already defined" suri)
+ else begin
+ let name = UriManager.name_of_uri uri in
+ let obj = Cic.Constant (name, body, ty, params, attrs) in
+ let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
+ CicEnvironment.add_type_checked_term uri (obj, ugraph);
+ MetadataDb.index_constant ~dbd ~uri ~body ~ty;
+ let new_stuff = save_object_to_disk status uri obj in
+ MatitaLog.message (sprintf "%s constant defined" suri);
+ { status with objects = new_stuff @ status.objects }
+ end
+
+let split_obj = function
+ | Cic.Constant (name, body, ty, _, attrs)
+ | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs)
+ | _ -> assert false
+
+let add_inductive_def
+ ~uri ~types ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph status
+=
+ let dbd = MatitaDb.instance () in
+ let suri = UriManager.string_of_uri uri in
+ if CicEnvironment.in_library uri then
+ command_error (sprintf "%s inductive type already defined" suri)
+ else begin
+ let name = UriManager.name_of_uri uri in
+ let obj = Cic.InductiveDefinition (types, params, leftno, attrs) in
+ let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
+ CicEnvironment.put_inductive_definition uri (obj, ugraph);
+ MetadataDb.index_inductive_def ~dbd ~uri ~types:types;
+ let new_stuff = save_object_to_disk status uri obj in
+ MatitaLog.message (sprintf "%s inductive type defined" suri);
+ let status = { status with objects = new_stuff @ status.objects } in
+ let elim sort status =
+ try
+ let obj = CicElim.elim_of ~sort uri 0 in
+ let (name, body, ty, attrs) = split_obj obj in
+ let suri = MatitaMisc.qualify status name ^ ".con" in
+ let uri = UriManager.uri_of_string suri in
+ (* TODO Zack: make CicElim returns a universe *)
+ let ugraph = CicUniv.empty_ugraph in
+ add_constant ~uri ?body ~ty ~attrs ~ugraph status;
+ with CicElim.Can_t_eliminate -> status
+ in
+ List.fold_left
+ (fun status sort -> elim sort status)
+ status
+ [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
+ end
+
+module OrderedUri =
+struct
+ type t = UriManager.uri * string
+ let compare (u1, _) (u2, _) = UriManager.compare u1 u2
+end
+
+module UriSet = Set.Make (OrderedUri)
+
+(* returns the uri of objects that were added in the meanwhile...
+ * status1 ----> status2
+ * assumption: objects defined in status2 are a superset of those defined in
+ * status1
+ *)
+let delta_status status1 status2 =
+ let module S = UriSet in
+ let diff l1 l2 =
+ let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
+ let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
+ let diff = S.diff s2 s1 in
+ S.fold (fun uri uris -> uri :: uris) diff []
+ in
+ diff status1.objects status2.objects
+
+let time_travel ~present ~past =
+ let list_of_objs_to_remove = List.rev (delta_status past present) in
+ (* List.rev is just for the debugging code, which otherwise may list both
+ * something.ind and something.ind#xpointer ... (ask Enrico :-) *)
+ let debug_list = ref [] in
+ List.iter (fun (x,p) ->
+ remove_object_from_disk x p;
+ (try
+ CicEnvironment.remove_obj x
+ with CicEnvironment.Object_not_found _ ->
+ MatitaLog.debug
+ (sprintf "time_travel removes from cache %s that is not in"
+ (UriManager.string_of_uri x)));
+ let l = MatitaDb.remove_uri x in
+ debug_list := UriManager.string_of_uri x :: !debug_list @ l)
+ list_of_objs_to_remove;
+
+ (* this is debug code
+ * idea: debug_list is the list of objects to be removed as computed from the
+ * db, while list_of_objs_to_remove is the same list but computer from the
+ * differences between statuses *)
+ let l1 = List.sort Pervasives.compare !debug_list in
+ let l2 = List.sort Pervasives.compare
+ (List.map (fun (x,_) -> UriManager.string_of_uri x) list_of_objs_to_remove)
+ in
+ let rec uniq = function
+ | [] -> []
+ | h::[] -> [h]
+ | h1::h2::tl when h1 = h2 -> uniq (h2 :: tl)
+ | h1::tl (* when h1 <> h2 *) -> h1 :: uniq tl
+ in
+ let l1 = uniq l1 in
+ let l2 = uniq l2 in
+ try
+ List.iter2 (fun x y -> if x <> y then raise Exit) l1 l2
+ with
+ | Invalid_argument _ | Exit ->
+ MatitaLog.debug "It seems you garbaged something...";
+ MatitaLog.debug "l1:";
+ List.iter MatitaLog.debug l1;
+ MatitaLog.debug "l2:";
+ List.iter MatitaLog.debug l2
+
+let alias_diff ~from status =
+ let module Map = DisambiguateTypes.Environment in
+ Map.fold
+ (fun domain_item codomain_item acc ->
+ if not (Map.mem domain_item from.aliases) then
+ Map.add domain_item codomain_item acc
+ else
+ acc)
+ status.aliases Map.empty
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val add_constant:
+ uri:UriManager.uri ->
+ ?body:Cic.term -> ty:Cic.term ->
+ ugraph:CicUniv.universe_graph ->
+ ?params:UriManager.uri list -> ?attrs:Cic.attribute list ->
+ MatitaTypes.status -> MatitaTypes.status
+
+val add_inductive_def:
+ uri:UriManager.uri ->
+ types:Cic.inductiveType list ->
+ ?params:UriManager.uri list -> ?leftno:int -> ?attrs:Cic.attribute list ->
+ ugraph:CicUniv.universe_graph ->
+ MatitaTypes.status -> MatitaTypes.status
+
+val time_travel:
+ present:MatitaTypes.status -> past:MatitaTypes.status -> unit
+
+ (** perform a diff between the aliases contained in two statuses, assuming
+ * that the second one can only have more aliases than the first one
+ * @return the list of aliases that should be added to aliases of from in
+ * order to be equal to aliases of the second argument *)
+val alias_diff: from:MatitaTypes.status -> MatitaTypes.status ->
+ DisambiguateTypes.environment
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+ (** user hit the cancel button *)
+exception Cancel
+
+ (** statement invoked in the wrong context (e.g. tactic with no ongoing proof)
+ *)
+exception Statement_error of string
+let statement_error msg = raise (Statement_error msg)
+
+exception Command_error of string
+let command_error msg = raise (Command_error msg)
+
+ (** parameters are: option name, error message *)
+exception Option_error of string * string
+
+exception Unbound_identifier of string
+
+type proof_status =
+ | No_proof
+ | Incomplete_proof of ProofEngineTypes.status
+ | Proof of ProofEngineTypes.proof
+ | Intermediate of Cic.metasenv
+ (* Status in which the proof could be while it is being processed by the
+ * engine. No status entering/exiting the engine could be in it. *)
+
+module StringMap = Map.Make (String)
+
+type option_value =
+ | String of string
+ | Int of int
+type options = option_value StringMap.t
+let no_options = StringMap.empty
+
+type status = {
+ aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ proof_status: proof_status;
+ options: options;
+ coercions: CoercGraph.coercions;
+ objects: (UriManager.uri * string) list;
+ (** in-scope objects, with their paths *)
+}
+
+let dump_status status =
+ MatitaLog.message "status.aliases:\n";
+ MatitaLog.message
+ (CicTextualParser2.EnvironmentP3.to_string status.aliases ^ "\n");
+ MatitaLog.message "status.proof_status:";
+ MatitaLog.message
+ (match status.proof_status with
+ | No_proof -> "no proof\n"
+ | Incomplete_proof _ -> "incomplete proof\n"
+ | Proof _ -> "proof\n"
+ | Intermediate _ -> "Intermediate\n");
+ MatitaLog.message "status.options\n";
+ StringMap.iter (fun k v ->
+ let v =
+ match v with
+ | String s -> s
+ | Int i -> string_of_int i
+ in
+ MatitaLog.message (k ^ "::=" ^ v)) status.options;
+ MatitaLog.message "status.coercions\n";
+ List.iter
+ (fun (u1,u2,u3) -> MatitaLog.message
+ ((UriManager.string_of_uri u1) ^
+ (UriManager.string_of_uri u2) ^
+ (UriManager.string_of_uri u3))) status.coercions;
+ MatitaLog.message "status.objects:\n";
+ List.iter
+ (fun (u,_) ->
+ MatitaLog.message (UriManager.string_of_uri u)) status.objects
+
+
+let get_option status name =
+ try
+ StringMap.find name status.options
+ with Not_found -> raise (Option_error (name, "not found"))
+
+let get_string_option status name =
+ match get_option status name with
+ | String s -> s
+ | _ -> raise (Option_error (name, "not a string value"))
+
+let set_option status name value =
+ let mangle_dir s =
+ let s = Str.global_replace (Str.regexp "//+") "/" s in
+ let s = Str.global_replace (Str.regexp "/$") "" s in
+ s
+ in
+ let types =
+ [ "baseuri", (`String, mangle_dir);
+ "basedir", (`String, mangle_dir);
+ ]
+ in
+ let ty_and_mangler =
+ try
+ List.assoc name types
+ with Not_found -> command_error (sprintf "Unknown option \"%s\"" name)
+ in
+ let value =
+ match ty_and_mangler with
+ | `String, f -> String (f value)
+ | `Int, f ->
+ (try
+ Int (int_of_string (f value))
+ with Failure _ ->
+ command_error (sprintf "Not an integer value \"%s\"" value))
+ in
+ { status with options = StringMap.add name value status.options }
+
+ (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
+class type console =
+ object
+ method clear : unit -> unit
+ method echo_error : string -> unit
+ method echo_message : string -> unit
+ method wrap_exn : 'a. (unit -> 'a) -> 'a option
+ method choose_uri : string list -> string
+ method show : ?msg:string -> unit -> unit
+ end
+
--- /dev/null
+(* Copyright (C) 2004-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+open Printf
+
+open MatitaTypes
+
+(** {2 Initialization} *)
+
+let arg_spec = [
+(* "-opt", Arg...., "set bla bla bla"; *)
+]
+let usage =
+ sprintf "MatitaC v%s\nUsage: matitac [option ...] file ...\nOptions:"
+ BuildTimeConf.version
+
+let _ =
+ Helm_registry.load_from "matita.conf.xml";
+ Http_getter.init ();
+ MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+ MatitaDb.clean_owner_environment ();
+ MatitaDb.create_owner_environment ()
+
+let scripts =
+ let acc = ref [] in
+ let add_script fname = acc := fname :: !acc in
+ Arg.parse arg_spec add_script usage;
+ List.rev !acc
+
+let run_script fname =
+ MatitaLog.message (sprintf "execution of %s started:" fname);
+ let is =
+ Stream.of_channel
+ (match fname with
+ | "stdin" -> stdin
+ | fname -> open_in fname)
+ in
+ let status = ref (Lazy.force MatitaEngine.initial_status) in
+ try
+ while true do
+ dump_status !status;
+ try
+ status := MatitaEngine.eval_from_stream !status is
+ with
+ | CicTextualParser2.Parse_error _ as exn ->
+ try
+ Stream.empty is;
+ raise End_of_file
+ with Stream.Failure -> raise exn
+ | exn ->
+ MatitaLog.error (Printexc.to_string exn);
+ raise exn
+ done
+ with
+ | End_of_file ->
+ MatitaLog.message (sprintf "execution of %s completed." fname);
+ Http_getter.sync_dump_file ();
+ exit(0)
+ | CicTextualParser2.Parse_error (floc,err) ->
+ let (x, y) = CicAst.loc_of_floc floc in
+ MatitaLog.message (sprintf "Parse error at %d-%d: %s" x y err);
+ Http_getter.sync_dump_file ();
+ exit 1
+
+
+let _ = List.iter run_script scripts
+
--- /dev/null
+set "baseuri" "cic:/matita/zack/aaa/".
+inductive nat:Set \def O:nat | S:nat \to nat.
+set "baseuri" "cic:/matita/zack/bbb/".
+inductive nat:Set \def O:nat | S:nat \to nat.
+alias id "nat" = "cic:/matita/zack/bbb/nat.ind#xpointer(1/1)".
+inductive c:Set \def c1: nat \to c.
--- /dev/null
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias symbol "and" (instance 0) = "logical and".
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+theorem a:\forall x:nat.x=x\land x=x.
+intro.
+split.
+goal 6.
\ No newline at end of file
--- /dev/null
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+theorem a:\forall x.x=x.
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+goal 5.
+exact nat.
+intro.
+reflexivity.
+qed.
\ No newline at end of file
projects / helm.git / commitdiff
