+++ /dev/null
-mathita
-*.cm[aiox]
-*.cmxa
-*.[ao]
+++ /dev/null
-mathitaGeneratedGui.cmo: mathitaGeneratedGui.cmi
-mathitaGeneratedGui.cmx: mathitaGeneratedGui.cmi
-mathitaGtkMisc.cmo: mathitaGtkMisc.cmi
-mathitaGtkMisc.cmx: mathitaGtkMisc.cmi
-mathitaGui.cmo: mathitaGeneratedGui.cmi mathitaGtkMisc.cmi mathitaGui.cmi
-mathitaGui.cmx: mathitaGeneratedGui.cmx mathitaGtkMisc.cmx mathitaGui.cmi
-mathita.cmo: mathitaGeneratedGui.cmi mathitaGui.cmi
-mathita.cmx: mathitaGeneratedGui.cmx mathitaGui.cmx
-mathitaGui.cmi: mathitaGeneratedGui.cmi mathitaGtkMisc.cmi
+++ /dev/null
-
-OCAMLFIND = ocamlfind
-REQUIRES = lablgtk2.glade helm-registry
-OCAML_FLAGS = -package "$(REQUIRES)" -pp camlp4o
-OCAML_THREADS_FLAGS = -thread
-OCAML_DEBUG_FLAGS =
-OCAMLC = $(OCAMLFIND) ocamlc $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS)
-OCAMLOPT = $(OCAMLFIND) opt $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS)
-OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS)
-LABLGLADECC = lablgladecc2
-CMOS = \
- mathitaGeneratedGui.cmo \
- mathitaGtkMisc.cmo \
- mathitaGui.cmo
-
-all: mathita
-
-mathita: $(CMOS) mathita.ml
- $(OCAMLC) -linkpkg -o $@ $^
-
-mathitaGeneratedGui.ml mathitaGeneratedGui.mli: mathita.glade
- $(LABLGLADECC) $< > $@
- $(OCAMLC) -i mathitaGeneratedGui.ml > mathitaGeneratedGui.mli
-
-%.cmi: %.mli
- $(OCAMLC) -c $<
-%.cmo %.cmi: %.ml
- $(OCAMLC) -c $<
-%.cmx: %.ml
- $(OCAMLOPT) -c $<
-%.ml %.mli: %.mly
- $(OCAMLYACC) $<
-
-clean:
- rm -rf *.cm[aoix] *.cmxa *.[ao] mathita
-distclean: clean
- rm -f mathitaGeneratedGui.ml
-
-depend: mathitaGeneratedGui.ml
- $(OCAMLDEP) *.ml *.mli > .depend
-
-include .depend
-
+++ /dev/null
-<?xml version="1.0" encoding="utf-8"?>
-<helm_registry>
- <section name="mathita">
- <key name="glade_file">mathita.glade</key>
- <key name="auto_disambiguation">true</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="GtkWindow" id="MainWin">
- <property name="visible">True</property>
- <property name="title" translatable="yes">Mathita</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>
-
- <child>
- <widget class="GtkVBox" id="MainWinShape">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
-
- <child>
- <widget class="GtkMenuBar" id="MainMenuBar">
- <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="NewMenu">
- <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="image40">
- <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>
-
- <child>
- <widget class="GtkMenu" id="NewMenu_menu">
-
- <child>
- <widget class="GtkMenuItem" id="NewProofMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">_Proof or definition ...</property>
- <property name="use_underline">True</property>
- <accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
- </widget>
- </child>
-
- <child>
- <widget class="GtkMenuItem" id="NewDefsMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">(Co)Inductive _definitions ...</property>
- <property name="use_underline">True</property>
- </widget>
- </child>
- </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="image41">
- <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="image42">
- <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="image43">
- <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="GtkMenuItem" id="separator1">
- <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="image44">
- <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="GtkCheckMenuItem" id="ShowToolBarMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">Show Button Bar</property>
- <property name="use_underline">True</property>
- <property name="active">True</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkCheckMenuItem" id="ShowProofMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">Show Proof Window</property>
- <property name="use_underline">True</property>
- <property name="active">False</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="GtkMenuItem" id="DebugMenuItem0">
- <property name="visible">True</property>
- <property name="label" translatable="yes">0</property>
- <property name="use_underline">True</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkMenuItem" id="DebugMenuItem1">
- <property name="visible">True</property>
- <property name="label" translatable="yes">1</property>
- <property name="use_underline">True</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkMenuItem" id="DebugMenuItem2">
- <property name="visible">True</property>
- <property name="label" translatable="yes">2</property>
- <property name="use_underline">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>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkVPaned" id="MainVPanes">
- <property name="visible">True</property>
- <property name="can_focus">True</property>
- <property name="position">450</property>
-
- <child>
- <widget class="GtkScrolledWindow" id="ProofStatus">
- <property name="visible">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>
- <placeholder/>
- </child>
- </widget>
- <packing>
- <property name="shrink">True</property>
- <property name="resize">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkScrolledWindow" id="ScrolledUserInput">
- <property name="visible">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>
- <placeholder/>
- </child>
- </widget>
- <packing>
- <property name="shrink">True</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>
-
- <child>
- <widget class="GtkStatusbar" id="MainStatusBar">
- <property name="visible">True</property>
- <property name="has_resize_grip">True</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="ProofWin">
- <property name="title" translatable="yes">Mathita: current proof</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">700</property>
- <property name="default_height">525</property>
- <property name="resizable">True</property>
- <property name="destroy_with_parent">False</property>
-
- <child>
- <widget class="GtkEventBox" id="ProofWinEventBox">
- <property name="visible">True</property>
-
- <child>
- <widget class="GtkScrolledWindow" id="ScrolledProof">
- <property name="visible">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="GtkViewport" id="viewport1">
- <property name="visible">True</property>
- <property name="shadow_type">GTK_SHADOW_IN</property>
-
- <child>
- <placeholder/>
- </child>
- </widget>
- </child>
- </widget>
- </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="show_fileops">True</property>
-
- <child internal-child="cancel_button">
- <widget class="GtkButton" id="cancel_button1">
- <property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- </widget>
- </child>
-
- <child internal-child="ok_button">
- <widget class="GtkButton" id="ok_button1">
- <property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- </widget>
- </child>
-</widget>
-
-<widget class="GtkWindow" id="ToolBarWin">
- <property name="width_request">130</property>
- <property name="height_request">450</property>
- <property name="visible">True</property>
- <property name="title" translatable="yes">ToolBar</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">False</property>
- <property name="destroy_with_parent">False</property>
-
- <child>
- <widget class="GtkEventBox" id="ToolBarEventBox">
- <property name="visible">True</property>
-
- <child>
- <widget class="GtkVBox" id="vbox1">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
-
- <child>
- <widget class="GtkVButtonBox" id="vbuttonbox1">
- <property name="visible">True</property>
- <property name="layout_style">GTK_BUTTONBOX_DEFAULT_STYLE</property>
- <property name="spacing">0</property>
-
- <child>
- <widget class="GtkButton" id="button1">
- <property name="width_request">120</property>
- <property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">button1</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkButton" id="button2">
- <property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">button2</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkButton" id="button3">
- <property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">button3</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkButton" id="button4">
- <property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">button4</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">True</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkHSeparator" id="hseparator1">
- <property name="visible">True</property>
- </widget>
- <packing>
- <property name="padding">5</property>
- <property name="expand">False</property>
- <property name="fill">True</property>
- </packing>
- </child>
-
- <child>
- <placeholder/>
- </child>
- </widget>
- </child>
- </widget>
- </child>
-</widget>
-
-<widget class="GtkDialog" id="GenericDialog">
- <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="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="cancelbutton1">
- <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="response_id">-6</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkButton" id="okbutton1">
- <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="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>
- <placeholder/>
- </child>
- </widget>
- </child>
-</widget>
-
-<widget class="GtkDialog" id="AboutWin">
- <property name="title" translatable="yes">Mathita: 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="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="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>
- <placeholder/>
- </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="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="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="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>
-
- <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="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="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>
-
- <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" translatable="yes">*</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>
-
-<widget class="GtkDialog" id="InterpChoiceDialog">
- <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="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="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="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="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="label6">
- <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>
- <placeholder/>
- </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="Debug">
- <property name="visible">True</property>
- <property name="title" translatable="yes">dialog1</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="has_separator">True</property>
-
- <child internal-child="vbox">
- <widget class="GtkVBox" id="dialog-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="dialog-action_area5">
- <property name="visible">True</property>
- <property name="layout_style">GTK_BUTTONBOX_END</property>
-
- <child>
- <widget class="GtkButton" id="cancelbutton2">
- <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="response_id">-6</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkButton" id="okbutton2">
- <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="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>
- <placeholder/>
- </child>
- </widget>
- </child>
-</widget>
-
-</glade-interface>
+++ /dev/null
-<?xml version="1.0" standalone="no"?> <!--*- mode: xml -*-->
-<!DOCTYPE glade-project SYSTEM "http://glade.gnome.org/glade-project-2.0.dtd">
-
-<glade-project>
- <name>Mathita</name>
- <program_name>mathita</program_name>
- <gnome_support>FALSE</gnome_support>
-</glade-project>
+++ /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/
- *)
-
-exception Not_implemented of string
-let not_implemented feature = raise (Not_implemented feature)
-
- (** exceptions whose content should be presented to the user *)
-exception Failure of string
-let error s = raise (Failure s)
-
-let _ = Helm_registry.load_from "mathita.conf.xml"
-let _ = GMain.Main.init ()
-let gui = new MathitaGui.gui (Helm_registry.get "mathita.glade_file")
-
-let interactive_user_uri_choice
- ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(nonvars_button=false) ~title ~msg
- uris
-=
- let only_constant_choices =
- lazy
- (List.filter
- (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
- uris)
- in
- if (selection_mode <> `SINGLE) &&
- (Helm_registry.get_bool "mathita.auto_disambiguation")
- then
- Lazy.force only_constant_choices
- else begin
- let win = gui#uriChoice in
- let choices = ref [] in
- let chosen = ref false in
- let use_only_constants = ref false in
- win#uriChoiceDialog#set_title title;
- win#uriChoiceLabel#set_text msg;
- gui#uriChoices#list_store#clear ();
- List.iter gui#uriChoices#easy_append uris;
- win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
- let bye = ref (fun () -> ()) in
- let id1 =
- win#uriChoiceConstantsButton#connect#clicked (fun _ ->
- use_only_constants := true;
- !bye ())
- in
- let id2 =
- win#uriChoiceAutoButton#connect#clicked (fun _ ->
- use_only_constants := true ;
- Helm_registry.set_bool "mathita.auto_disambiguation" true;
- !bye ())
- in
- let id3 =
- win#uriChoiceSelectedButton#connect#clicked (fun _ ->
- choices := gui#uriChoices#easy_selection ();
- !bye ())
- in
- bye := (fun () ->
- win#uriChoiceDialog#misc#hide ();
- win#uriChoiceConstantsButton#misc#disconnect id1;
- win#uriChoiceAutoButton#misc#disconnect id2;
- win#uriChoiceSelectedButton#misc#disconnect id3;
- prerr_endline "quit";
- GMain.Main.quit ());
- win#uriChoiceDialog#show ();
- GtkThread.main ();
- if !use_only_constants then
- Lazy.force only_constant_choices
- else
- match !choices with
- | [] -> error "No choice"
- | choices -> choices
- end
-
-(*
-module DisambiguateCallbacks =
- struct
- let interactive_user_uri_choice =
- assert false (* TODO *)
-(* interactive_user_uri_choice *)
- let interactive_interpretation_choice choices =
- assert false (* TODO *)
- let input_or_locate_uri ~title =
- assert false (* TODO *)
- end
-*)
-
-let debugDialog () =
- let dialog =
- new MathitaGeneratedGui.debug
- ~file:(Helm_registry.get "mathita.glade_file") ()
- in
- let retval = ref None in
- let return v =
- retval := Some v;
- dialog#debug#destroy ();
- GMain.Main.quit ()
- in
- ignore (dialog#debug#event#connect#delete (fun _ -> true));
- ignore (dialog#okbutton2#connect#clicked (fun _ -> return 1));
- ignore (dialog#cancelbutton2#connect#clicked (fun _ -> return 2));
- dialog#debug#show ();
- GtkThread.main ();
- (match !retval with None -> assert false | Some v -> v)
-
-let _ =
- gui#main#debugMenuItem2#connect#activate (fun _ ->
- prerr_endline (string_of_int (debugDialog ())))
-
- (** quit program, possibly asking for confirmation *)
-let quit () = GMain.Main.quit ()
-let _ = gui#setQuitCallback quit
-let _ =
- gui#main#debugMenuItem0#connect#activate (fun _ ->
- let uris =
- interactive_user_uri_choice
- ~selection_mode:`MULTIPLE
- ~nonvars_button:false
- ~title:"titolo"
- ~msg:"messaggio"
- ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
- "cic:/cinque.var"]
- in
- List.iter prerr_endline uris; print_newline ())
-let _ =
- gui#main#debugMenuItem1#connect#activate (fun _ ->
- Helm_registry.set_bool "mathita.auto_disambiguation"
- (not (Helm_registry.get_bool "mathita.auto_disambiguation")))
-
-let _ =
-(* gui#uriChoices#easy_append "pippo"; *)
-(* gui#uriChoices#list_store#clear (); *)
- GtkThread.main ()
-
+++ /dev/null
-(* Automatically generated from mathita.glade by lablgladecc *)
-
-class mainWin ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"MainWin" ?domain () in
- object (self)
- inherit Glade.xml ?autoconnect xmldata
- val toplevel =
- new GWindow.window (GtkWindow.Window.cast
- (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata))
- method toplevel = toplevel
- val mainWin =
- new GWindow.window (GtkWindow.Window.cast
- (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata))
- method mainWin = mainWin
- val mainWinShape =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"MainWinShape" ~info:"GtkVBox" xmldata))
- method mainWinShape = mainWinShape
- val mainMenuBar =
- new GMenu.menu_shell (GtkMenu.MenuBar.cast
- (Glade.get_widget_msg ~name:"MainMenuBar" ~info:"GtkMenuBar" xmldata))
- method mainMenuBar = mainMenuBar
- val fileMenu =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"FileMenu" ~info:"GtkMenuItem" xmldata))
- method fileMenu = fileMenu
- val fileMenu_menu =
- new GMenu.menu (GtkMenu.Menu.cast
- (Glade.get_widget_msg ~name:"FileMenu_menu" ~info:"GtkMenu" xmldata))
- method fileMenu_menu = fileMenu_menu
- val newMenu =
- new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
- (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
- method newMenu = newMenu
- val image40 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image40" ~info:"GtkImage" xmldata))
- method image40 = image40
- val newMenu_menu =
- new GMenu.menu (GtkMenu.Menu.cast
- (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata))
- method newMenu_menu = newMenu_menu
- val newProofMenuItem =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"NewProofMenuItem" ~info:"GtkMenuItem" xmldata))
- method newProofMenuItem = newProofMenuItem
- val newDefsMenuItem =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"NewDefsMenuItem" ~info:"GtkMenuItem" xmldata))
- method newDefsMenuItem = newDefsMenuItem
- val openMenuItem =
- new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
- (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata))
- method openMenuItem = openMenuItem
- val image41 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image41" ~info:"GtkImage" xmldata))
- method image41 = image41
- val saveMenuItem =
- new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
- (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
- method saveMenuItem = saveMenuItem
- val image42 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image42" ~info:"GtkImage" xmldata))
- method image42 = image42
- val saveAsMenuItem =
- new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
- (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
- method saveAsMenuItem = saveAsMenuItem
- val image43 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image43" ~info:"GtkImage" xmldata))
- method image43 = image43
- val separator1 =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"separator1" ~info:"GtkMenuItem" xmldata))
- method separator1 = separator1
- val quitMenuItem =
- new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
- (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata))
- method quitMenuItem = quitMenuItem
- val image44 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image44" ~info:"GtkImage" xmldata))
- method image44 = image44
- val editMenu =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))
- method editMenu = editMenu
- val viewMenu =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"ViewMenu" ~info:"GtkMenuItem" xmldata))
- method viewMenu = viewMenu
- val viewMenu_menu =
- new GMenu.menu (GtkMenu.Menu.cast
- (Glade.get_widget_msg ~name:"ViewMenu_menu" ~info:"GtkMenu" xmldata))
- method viewMenu_menu = viewMenu_menu
- val showToolBarMenuItem =
- new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
- (Glade.get_widget_msg ~name:"ShowToolBarMenuItem" ~info:"GtkCheckMenuItem" xmldata))
- method showToolBarMenuItem = showToolBarMenuItem
- val showProofMenuItem =
- new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
- (Glade.get_widget_msg ~name:"ShowProofMenuItem" ~info:"GtkCheckMenuItem" xmldata))
- method showProofMenuItem = showProofMenuItem
- val debugMenu =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata))
- method debugMenu = debugMenu
- val debugMenu_menu =
- new GMenu.menu (GtkMenu.Menu.cast
- (Glade.get_widget_msg ~name:"DebugMenu_menu" ~info:"GtkMenu" xmldata))
- method debugMenu_menu = debugMenu_menu
- val debugMenuItem0 =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"DebugMenuItem0" ~info:"GtkMenuItem" xmldata))
- method debugMenuItem0 = debugMenuItem0
- val debugMenuItem1 =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"DebugMenuItem1" ~info:"GtkMenuItem" xmldata))
- method debugMenuItem1 = debugMenuItem1
- val debugMenuItem2 =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"DebugMenuItem2" ~info:"GtkMenuItem" xmldata))
- method debugMenuItem2 = debugMenuItem2
- val helpMenu =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"HelpMenu" ~info:"GtkMenuItem" xmldata))
- method helpMenu = helpMenu
- val helpMenu_menu =
- new GMenu.menu (GtkMenu.Menu.cast
- (Glade.get_widget_msg ~name:"HelpMenu_menu" ~info:"GtkMenu" xmldata))
- method helpMenu_menu = helpMenu_menu
- val aboutMenuItem =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"AboutMenuItem" ~info:"GtkMenuItem" xmldata))
- method aboutMenuItem = aboutMenuItem
- val mainVPanes =
- new GPack.paned (GtkPack.Paned.cast
- (Glade.get_widget_msg ~name:"MainVPanes" ~info:"GtkVPaned" xmldata))
- method mainVPanes = mainVPanes
- val proofStatus =
- new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
- (Glade.get_widget_msg ~name:"ProofStatus" ~info:"GtkScrolledWindow" xmldata))
- method proofStatus = proofStatus
- val scrolledUserInput =
- new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
- (Glade.get_widget_msg ~name:"ScrolledUserInput" ~info:"GtkScrolledWindow" xmldata))
- method scrolledUserInput = scrolledUserInput
- val mainStatusBar =
- new GMisc.statusbar (GtkMisc.Statusbar.cast
- (Glade.get_widget_msg ~name:"MainStatusBar" ~info:"GtkStatusbar" xmldata))
- method mainStatusBar = mainStatusBar
- method reparent parent =
- mainWinShape#misc#reparent parent;
- toplevel#destroy ()
- method check_widgets () = ()
- end
-class proofWin ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"ProofWin" ?domain () in
- object (self)
- inherit Glade.xml ?autoconnect xmldata
- val toplevel =
- new GWindow.window (GtkWindow.Window.cast
- (Glade.get_widget_msg ~name:"ProofWin" ~info:"GtkWindow" xmldata))
- method toplevel = toplevel
- val proofWin =
- new GWindow.window (GtkWindow.Window.cast
- (Glade.get_widget_msg ~name:"ProofWin" ~info:"GtkWindow" xmldata))
- method proofWin = proofWin
- val proofWinEventBox =
- new GBin.event_box (GtkBin.EventBox.cast
- (Glade.get_widget_msg ~name:"ProofWinEventBox" ~info:"GtkEventBox" xmldata))
- method proofWinEventBox = proofWinEventBox
- val scrolledProof =
- new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
- (Glade.get_widget_msg ~name:"ScrolledProof" ~info:"GtkScrolledWindow" xmldata))
- method scrolledProof = scrolledProof
- val viewport1 =
- new GBin.viewport (GtkBin.Viewport.cast
- (Glade.get_widget_msg ~name:"viewport1" ~info:"GtkViewport" xmldata))
- method viewport1 = viewport1
- method reparent parent =
- proofWinEventBox#misc#reparent parent;
- toplevel#destroy ()
- method check_widgets () = ()
- end
-class fileSelectionWin ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"FileSelectionWin" ?domain () in
- object (self)
- inherit Glade.xml ?autoconnect xmldata
- val toplevel =
- new GWindow.file_selection (GtkWindow.FileSelection.cast
- (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata))
- method toplevel = toplevel
- val fileSelectionWin =
- new GWindow.file_selection (GtkWindow.FileSelection.cast
- (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata))
- method fileSelectionWin = fileSelectionWin
- val cancel_button1 =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"cancel_button1" ~info:"GtkButton" xmldata))
- method cancel_button1 = cancel_button1
- val ok_button1 =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"ok_button1" ~info:"GtkButton" xmldata))
- method ok_button1 = ok_button1
- method check_widgets () = ()
- end
-class toolBarWin ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"ToolBarWin" ?domain () in
- object (self)
- inherit Glade.xml ?autoconnect xmldata
- val toplevel =
- new GWindow.window (GtkWindow.Window.cast
- (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata))
- method toplevel = toplevel
- val toolBarWin =
- new GWindow.window (GtkWindow.Window.cast
- (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata))
- method toolBarWin = toolBarWin
- val toolBarEventBox =
- new GBin.event_box (GtkBin.EventBox.cast
- (Glade.get_widget_msg ~name:"ToolBarEventBox" ~info:"GtkEventBox" xmldata))
- method toolBarEventBox = toolBarEventBox
- val vbox1 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"vbox1" ~info:"GtkVBox" xmldata))
- method vbox1 = vbox1
- val button1 =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"button1" ~info:"GtkButton" xmldata))
- method button1 = button1
- val button2 =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"button2" ~info:"GtkButton" xmldata))
- method button2 = button2
- val button3 =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"button3" ~info:"GtkButton" xmldata))
- method button3 = button3
- val button4 =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"button4" ~info:"GtkButton" xmldata))
- method button4 = button4
- method reparent parent =
- toolBarEventBox#misc#reparent parent;
- toplevel#destroy ()
- method check_widgets () = ()
- end
-class genericDialog ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"GenericDialog" ?domain () in
- object (self)
- inherit Glade.xml ?autoconnect xmldata
- val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
- new GWindow.dialog (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"GenericDialog" ~info:"GtkDialog" xmldata))
- method toplevel = toplevel
- val genericDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
- new GWindow.dialog (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"GenericDialog" ~info:"GtkDialog" xmldata))
- method genericDialog = genericDialog
- val dialog_vbox1 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"dialog-vbox1" ~info:"GtkVBox" xmldata))
- method dialog_vbox1 = dialog_vbox1
- val cancelbutton1 =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"cancelbutton1" ~info:"GtkButton" xmldata))
- method cancelbutton1 = cancelbutton1
- val okbutton1 =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"okbutton1" ~info:"GtkButton" xmldata))
- method okbutton1 = okbutton1
- method reparent parent =
- dialog_vbox1#misc#reparent parent;
- toplevel#destroy ()
- method check_widgets () = ()
- end
-class aboutWin ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"AboutWin" ?domain () in
- object (self)
- inherit Glade.xml ?autoconnect xmldata
- val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
- new GWindow.dialog (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"AboutWin" ~info:"GtkDialog" xmldata))
- method toplevel = toplevel
- val aboutWin : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
- new GWindow.dialog (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"AboutWin" ~info:"GtkDialog" xmldata))
- method aboutWin = aboutWin
- val dialog_vbox2 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"dialog-vbox2" ~info:"GtkVBox" xmldata))
- method dialog_vbox2 = dialog_vbox2
- val aboutDismissButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"AboutDismissButton" ~info:"GtkButton" xmldata))
- method aboutDismissButton = aboutDismissButton
- method reparent parent =
- dialog_vbox2#misc#reparent parent;
- toplevel#destroy ()
- method check_widgets () = ()
- end
-class uriChoiceDialog ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"UriChoiceDialog" ?domain () in
- object (self)
- inherit Glade.xml ?autoconnect xmldata
- val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
- new GWindow.dialog (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata))
- method toplevel = toplevel
- val uriChoiceDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
- new GWindow.dialog (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata))
- method uriChoiceDialog = uriChoiceDialog
- val dialog_vbox3 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"dialog-vbox3" ~info:"GtkVBox" xmldata))
- method dialog_vbox3 = dialog_vbox3
- val uriChoiceAbortButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"UriChoiceAbortButton" ~info:"GtkButton" xmldata))
- method uriChoiceAbortButton = uriChoiceAbortButton
- val uriChoiceSelectedButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"UriChoiceSelectedButton" ~info:"GtkButton" xmldata))
- method uriChoiceSelectedButton = uriChoiceSelectedButton
- val alignment2 =
- new GBin.alignment (GtkBin.Alignment.cast
- (Glade.get_widget_msg ~name:"alignment2" ~info:"GtkAlignment" xmldata))
- method alignment2 = alignment2
- val hbox3 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"hbox3" ~info:"GtkHBox" xmldata))
- method hbox3 = hbox3
- val image19 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image19" ~info:"GtkImage" xmldata))
- method image19 = image19
- val label3 =
- new GMisc.label (GtkMisc.Label.cast
- (Glade.get_widget_msg ~name:"label3" ~info:"GtkLabel" xmldata))
- method label3 = label3
- val uriChoiceConstantsButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"UriChoiceConstantsButton" ~info:"GtkButton" xmldata))
- method uriChoiceConstantsButton = uriChoiceConstantsButton
- val uriChoiceAutoButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"UriChoiceAutoButton" ~info:"GtkButton" xmldata))
- method uriChoiceAutoButton = uriChoiceAutoButton
- val alignment1 =
- new GBin.alignment (GtkBin.Alignment.cast
- (Glade.get_widget_msg ~name:"alignment1" ~info:"GtkAlignment" xmldata))
- method alignment1 = alignment1
- val hbox1 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"hbox1" ~info:"GtkHBox" xmldata))
- method hbox1 = hbox1
- val image18 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image18" ~info:"GtkImage" xmldata))
- method image18 = image18
- val label1 =
- new GMisc.label (GtkMisc.Label.cast
- (Glade.get_widget_msg ~name:"label1" ~info:"GtkLabel" xmldata))
- method label1 = label1
- val vbox2 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"vbox2" ~info:"GtkVBox" xmldata))
- method vbox2 = vbox2
- val uriChoiceLabel =
- new GMisc.label (GtkMisc.Label.cast
- (Glade.get_widget_msg ~name:"UriChoiceLabel" ~info:"GtkLabel" xmldata))
- method uriChoiceLabel = uriChoiceLabel
- val scrolledwindow1 =
- new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
- (Glade.get_widget_msg ~name:"scrolledwindow1" ~info:"GtkScrolledWindow" xmldata))
- method scrolledwindow1 = scrolledwindow1
- val uriChoiceTreeView =
- new GTree.view (GtkTree.TreeView.cast
- (Glade.get_widget_msg ~name:"UriChoiceTreeView" ~info:"GtkTreeView" xmldata))
- method uriChoiceTreeView = uriChoiceTreeView
- val hbox2 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"hbox2" ~info:"GtkHBox" xmldata))
- method hbox2 = hbox2
- val label2 =
- new GMisc.label (GtkMisc.Label.cast
- (Glade.get_widget_msg ~name:"label2" ~info:"GtkLabel" xmldata))
- method label2 = label2
- val entry1 =
- new GEdit.entry (GtkEdit.Entry.cast
- (Glade.get_widget_msg ~name:"entry1" ~info:"GtkEntry" xmldata))
- method entry1 = entry1
- method reparent parent =
- dialog_vbox3#misc#reparent parent;
- toplevel#destroy ()
- method check_widgets () = ()
- end
-class interpChoiceDialog ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"InterpChoiceDialog" ?domain () in
- object (self)
- inherit Glade.xml ?autoconnect xmldata
- val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
- new GWindow.dialog (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"InterpChoiceDialog" ~info:"GtkDialog" xmldata))
- method toplevel = toplevel
- val interpChoiceDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
- new GWindow.dialog (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"InterpChoiceDialog" ~info:"GtkDialog" xmldata))
- method interpChoiceDialog = interpChoiceDialog
- val dialog_vbox4 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"dialog-vbox4" ~info:"GtkVBox" xmldata))
- method dialog_vbox4 = dialog_vbox4
- val interpChoiceHelpButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"InterpChoiceHelpButton" ~info:"GtkButton" xmldata))
- method interpChoiceHelpButton = interpChoiceHelpButton
- val interpChoiceCancelButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"InterpChoiceCancelButton" ~info:"GtkButton" xmldata))
- method interpChoiceCancelButton = interpChoiceCancelButton
- val interpChoiceOkButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"InterpChoiceOkButton" ~info:"GtkButton" xmldata))
- method interpChoiceOkButton = interpChoiceOkButton
- val vbox3 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"vbox3" ~info:"GtkVBox" xmldata))
- method vbox3 = vbox3
- val label6 =
- new GMisc.label (GtkMisc.Label.cast
- (Glade.get_widget_msg ~name:"label6" ~info:"GtkLabel" xmldata))
- method label6 = label6
- method reparent parent =
- dialog_vbox4#misc#reparent parent;
- toplevel#destroy ()
- method check_widgets () = ()
- end
-class debug ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"Debug" ?domain () in
- object (self)
- inherit Glade.xml ?autoconnect xmldata
- val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
- new GWindow.dialog (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata))
- method toplevel = toplevel
- val debug : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
- new GWindow.dialog (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata))
- method debug = debug
- val dialog_vbox5 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"dialog-vbox5" ~info:"GtkVBox" xmldata))
- method dialog_vbox5 = dialog_vbox5
- val cancelbutton2 =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"cancelbutton2" ~info:"GtkButton" xmldata))
- method cancelbutton2 = cancelbutton2
- val okbutton2 =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"okbutton2" ~info:"GtkButton" xmldata))
- method okbutton2 = okbutton2
- method reparent parent =
- dialog_vbox5#misc#reparent parent;
- toplevel#destroy ()
- method check_widgets () = ()
- end
-
-let check_all ?(show=false) () =
- ignore (GMain.Main.init ());
- let debug = new debug () in
- if show then debug#toplevel#show ();
- debug#check_widgets ();
- let interpChoiceDialog = new interpChoiceDialog () in
- if show then interpChoiceDialog#toplevel#show ();
- interpChoiceDialog#check_widgets ();
- let uriChoiceDialog = new uriChoiceDialog () in
- if show then uriChoiceDialog#toplevel#show ();
- uriChoiceDialog#check_widgets ();
- let aboutWin = new aboutWin () in
- if show then aboutWin#toplevel#show ();
- aboutWin#check_widgets ();
- let genericDialog = new genericDialog () in
- if show then genericDialog#toplevel#show ();
- genericDialog#check_widgets ();
- let toolBarWin = new toolBarWin () in
- if show then toolBarWin#toplevel#show ();
- toolBarWin#check_widgets ();
- let fileSelectionWin = new fileSelectionWin () in
- if show then fileSelectionWin#toplevel#show ();
- fileSelectionWin#check_widgets ();
- let proofWin = new proofWin () in
- if show then proofWin#toplevel#show ();
- proofWin#check_widgets ();
- let mainWin = new mainWin () in
- if show then mainWin#toplevel#show ();
- mainWin#check_widgets ();
- if show then GMain.Main.main ()
-;;
+++ /dev/null
-class mainWin :
- ?file:string ->
- ?domain:string ->
- ?autoconnect:bool ->
- unit ->
- object
- val aboutMenuItem : GMenu.menu_item
- val debugMenu : GMenu.menu_item
- val debugMenuItem0 : GMenu.menu_item
- val debugMenuItem1 : GMenu.menu_item
- val debugMenuItem2 : GMenu.menu_item
- val debugMenu_menu : GMenu.menu
- val editMenu : GMenu.menu_item
- val fileMenu : GMenu.menu_item
- val fileMenu_menu : GMenu.menu
- val helpMenu : GMenu.menu_item
- val helpMenu_menu : GMenu.menu
- val image40 : GMisc.image
- val image41 : GMisc.image
- val image42 : GMisc.image
- val image43 : GMisc.image
- val image44 : GMisc.image
- val mainMenuBar : GMenu.menu_shell
- val mainStatusBar : GMisc.statusbar
- val mainVPanes : GPack.paned
- val mainWin : GWindow.window
- val mainWinShape : GPack.box
- val newDefsMenuItem : GMenu.menu_item
- val newMenu : GMenu.image_menu_item
- val newMenu_menu : GMenu.menu
- val newProofMenuItem : GMenu.menu_item
- val openMenuItem : GMenu.image_menu_item
- val proofStatus : GBin.scrolled_window
- val quitMenuItem : GMenu.image_menu_item
- val saveAsMenuItem : GMenu.image_menu_item
- val saveMenuItem : GMenu.image_menu_item
- val scrolledUserInput : GBin.scrolled_window
- val separator1 : GMenu.menu_item
- val showProofMenuItem : GMenu.check_menu_item
- val showToolBarMenuItem : GMenu.check_menu_item
- val toplevel : GWindow.window
- val viewMenu : GMenu.menu_item
- val viewMenu_menu : GMenu.menu
- val xml : Glade.glade_xml Gtk.obj
- method aboutMenuItem : GMenu.menu_item
- method bind : name:string -> callback:(unit -> unit) -> unit
- method check_widgets : unit -> unit
- method debugMenu : GMenu.menu_item
- method debugMenuItem0 : GMenu.menu_item
- method debugMenuItem1 : GMenu.menu_item
- method debugMenuItem2 : GMenu.menu_item
- method debugMenu_menu : GMenu.menu
- method editMenu : GMenu.menu_item
- method fileMenu : GMenu.menu_item
- method fileMenu_menu : GMenu.menu
- method helpMenu : GMenu.menu_item
- method helpMenu_menu : GMenu.menu
- method image40 : GMisc.image
- method image41 : GMisc.image
- method image42 : GMisc.image
- method image43 : GMisc.image
- method image44 : GMisc.image
- method mainMenuBar : GMenu.menu_shell
- method mainStatusBar : GMisc.statusbar
- method mainVPanes : GPack.paned
- method mainWin : GWindow.window
- method mainWinShape : GPack.box
- method newDefsMenuItem : GMenu.menu_item
- method newMenu : GMenu.image_menu_item
- method newMenu_menu : GMenu.menu
- method newProofMenuItem : GMenu.menu_item
- method openMenuItem : GMenu.image_menu_item
- method proofStatus : GBin.scrolled_window
- method quitMenuItem : GMenu.image_menu_item
- method reparent : GObj.widget -> unit
- method saveAsMenuItem : GMenu.image_menu_item
- method saveMenuItem : GMenu.image_menu_item
- method scrolledUserInput : GBin.scrolled_window
- method separator1 : GMenu.menu_item
- method showProofMenuItem : GMenu.check_menu_item
- method showToolBarMenuItem : GMenu.check_menu_item
- method toplevel : GWindow.window
- method viewMenu : GMenu.menu_item
- method viewMenu_menu : GMenu.menu
- method xml : Glade.glade_xml Gtk.obj
- end
-class proofWin :
- ?file:string ->
- ?domain:string ->
- ?autoconnect:bool ->
- unit ->
- object
- val proofWin : GWindow.window
- val proofWinEventBox : GBin.event_box
- val scrolledProof : GBin.scrolled_window
- val toplevel : GWindow.window
- val viewport1 : GBin.viewport
- val xml : Glade.glade_xml Gtk.obj
- method bind : name:string -> callback:(unit -> unit) -> unit
- method check_widgets : unit -> unit
- method proofWin : GWindow.window
- method proofWinEventBox : GBin.event_box
- method reparent : GObj.widget -> unit
- method scrolledProof : GBin.scrolled_window
- method toplevel : GWindow.window
- method viewport1 : GBin.viewport
- method xml : Glade.glade_xml Gtk.obj
- end
-class fileSelectionWin :
- ?file:string ->
- ?domain:string ->
- ?autoconnect:bool ->
- unit ->
- object
- val cancel_button1 : GButton.button
- val fileSelectionWin : GWindow.file_selection
- val ok_button1 : GButton.button
- val toplevel : GWindow.file_selection
- val xml : Glade.glade_xml Gtk.obj
- method bind : name:string -> callback:(unit -> unit) -> unit
- method cancel_button1 : GButton.button
- method check_widgets : unit -> unit
- method fileSelectionWin : GWindow.file_selection
- method ok_button1 : GButton.button
- method toplevel : GWindow.file_selection
- method xml : Glade.glade_xml Gtk.obj
- end
-class toolBarWin :
- ?file:string ->
- ?domain:string ->
- ?autoconnect:bool ->
- unit ->
- object
- val button1 : GButton.button
- val button2 : GButton.button
- val button3 : GButton.button
- val button4 : GButton.button
- val toolBarEventBox : GBin.event_box
- val toolBarWin : GWindow.window
- val toplevel : GWindow.window
- val vbox1 : GPack.box
- val xml : Glade.glade_xml Gtk.obj
- method bind : name:string -> callback:(unit -> unit) -> unit
- method button1 : GButton.button
- method button2 : GButton.button
- method button3 : GButton.button
- method button4 : GButton.button
- method check_widgets : unit -> unit
- method reparent : GObj.widget -> unit
- method toolBarEventBox : GBin.event_box
- method toolBarWin : GWindow.window
- method toplevel : GWindow.window
- method vbox1 : GPack.box
- method xml : Glade.glade_xml Gtk.obj
- end
-class genericDialog :
- ?file:string ->
- ?domain:string ->
- ?autoconnect:bool ->
- unit ->
- object
- val cancelbutton1 : GButton.button
- val dialog_vbox1 : GPack.box
- val genericDialog : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- val okbutton1 : GButton.button
- val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- val xml : Glade.glade_xml Gtk.obj
- method bind : name:string -> callback:(unit -> unit) -> unit
- method cancelbutton1 : GButton.button
- method check_widgets : unit -> unit
- method dialog_vbox1 : GPack.box
- method genericDialog :
- [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- method okbutton1 : GButton.button
- method reparent : GObj.widget -> unit
- method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- method xml : Glade.glade_xml Gtk.obj
- end
-class aboutWin :
- ?file:string ->
- ?domain:string ->
- ?autoconnect:bool ->
- unit ->
- object
- val aboutDismissButton : GButton.button
- val aboutWin : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- val dialog_vbox2 : GPack.box
- val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- val xml : Glade.glade_xml Gtk.obj
- method aboutDismissButton : GButton.button
- method aboutWin : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- method bind : name:string -> callback:(unit -> unit) -> unit
- method check_widgets : unit -> unit
- method dialog_vbox2 : GPack.box
- method reparent : GObj.widget -> unit
- method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- method xml : Glade.glade_xml Gtk.obj
- end
-class uriChoiceDialog :
- ?file:string ->
- ?domain:string ->
- ?autoconnect:bool ->
- unit ->
- object
- val alignment1 : GBin.alignment
- val alignment2 : GBin.alignment
- val dialog_vbox3 : GPack.box
- val entry1 : GEdit.entry
- val hbox1 : GPack.box
- val hbox2 : GPack.box
- val hbox3 : GPack.box
- val image18 : GMisc.image
- val image19 : GMisc.image
- val label1 : GMisc.label
- val label2 : GMisc.label
- val label3 : GMisc.label
- val scrolledwindow1 : GBin.scrolled_window
- val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- val uriChoiceAbortButton : GButton.button
- val uriChoiceAutoButton : GButton.button
- val uriChoiceConstantsButton : GButton.button
- val uriChoiceDialog :
- [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- val uriChoiceLabel : GMisc.label
- val uriChoiceSelectedButton : GButton.button
- val uriChoiceTreeView : GTree.view
- val vbox2 : GPack.box
- val xml : Glade.glade_xml Gtk.obj
- method alignment1 : GBin.alignment
- method alignment2 : GBin.alignment
- method bind : name:string -> callback:(unit -> unit) -> unit
- method check_widgets : unit -> unit
- method dialog_vbox3 : GPack.box
- method entry1 : GEdit.entry
- method hbox1 : GPack.box
- method hbox2 : GPack.box
- method hbox3 : GPack.box
- method image18 : GMisc.image
- method image19 : GMisc.image
- method label1 : GMisc.label
- method label2 : GMisc.label
- method label3 : GMisc.label
- method reparent : GObj.widget -> unit
- method scrolledwindow1 : GBin.scrolled_window
- method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- method uriChoiceAbortButton : GButton.button
- method uriChoiceAutoButton : GButton.button
- method uriChoiceConstantsButton : GButton.button
- method uriChoiceDialog :
- [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- method uriChoiceLabel : GMisc.label
- method uriChoiceSelectedButton : GButton.button
- method uriChoiceTreeView : GTree.view
- method vbox2 : GPack.box
- method xml : Glade.glade_xml Gtk.obj
- end
-class interpChoiceDialog :
- ?file:string ->
- ?domain:string ->
- ?autoconnect:bool ->
- unit ->
- object
- val dialog_vbox4 : GPack.box
- val interpChoiceCancelButton : GButton.button
- val interpChoiceDialog :
- [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- val interpChoiceHelpButton : GButton.button
- val interpChoiceOkButton : GButton.button
- val label6 : GMisc.label
- val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- val vbox3 : GPack.box
- val xml : Glade.glade_xml Gtk.obj
- method bind : name:string -> callback:(unit -> unit) -> unit
- method check_widgets : unit -> unit
- method dialog_vbox4 : GPack.box
- method interpChoiceCancelButton : GButton.button
- method interpChoiceDialog :
- [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- method interpChoiceHelpButton : GButton.button
- method interpChoiceOkButton : GButton.button
- method label6 : GMisc.label
- method reparent : GObj.widget -> unit
- method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- method vbox3 : GPack.box
- method xml : Glade.glade_xml Gtk.obj
- end
-class debug :
- ?file:string ->
- ?domain:string ->
- ?autoconnect:bool ->
- unit ->
- object
- val cancelbutton2 : GButton.button
- val debug : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- val dialog_vbox5 : GPack.box
- val okbutton2 : GButton.button
- val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- val xml : Glade.glade_xml Gtk.obj
- method bind : name:string -> callback:(unit -> unit) -> unit
- method cancelbutton2 : GButton.button
- method check_widgets : unit -> unit
- method debug : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- method dialog_vbox5 : GPack.box
- method okbutton2 : GButton.button
- method reparent : GObj.widget -> unit
- method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- method xml : Glade.glade_xml Gtk.obj
- end
-val check_all : ?show:bool -> unit -> unit
+++ /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 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
-
+++ /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/
- *)
-
-(** {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
-
- (** 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
-
+++ /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/
- *)
-
-(*
-class stringListModel' uriChoiceDialog =
- let tree_view = uriChoiceDialog#uriChoiceTreeView in
- 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
- let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in
- let view_column = GTree.view_column ~renderer () in
- let _ = tree_view#set_model (Some (list_store :> GTree.model)) in
- let _ = tree_view#append_column view_column in
- object
- method append s =
- let tree_iter = list_store#append () in
- list_store#set ~row:tree_iter ~column:text_column s
- method clear () = list_store#clear ()
- end
-*)
-
-open MathitaGeneratedGui
-open MathitaGtkMisc
-
-class gui file =
- (* creation order _is_ relevant for windows placement *)
- let toolbar = new toolBarWin ~file () in
- let main = new mainWin ~file () in
- let about = new aboutWin ~file () in
- let dialog = new genericDialog ~file () in
- let uriChoice = new uriChoiceDialog ~file () in
- let interpChoice = new interpChoiceDialog ~file () in
- let fileSel = new fileSelectionWin ~file () in
- let proof = new proofWin ~file () in
- let keyBindingBoxes = (* event boxes which should receive global key events *)
- [ toolbar#toolBarEventBox; proof#proofWinEventBox ]
- in
- let uriChoices = new stringListModel uriChoice#uriChoiceTreeView in
- object (self)
- initializer
- (* glade's check widgets *)
- List.iter (fun w -> w#check_widgets ())
- (let c w = (w :> <check_widgets: unit -> unit>) in
- [ c about; c dialog; c fileSel; c main; c proof; c toolbar;
- c uriChoice; c interpChoice ]);
- (* show/hide commands *)
- toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
- toggle_visibility proof#proofWin main#showProofMenuItem;
- (* "global" key bindings *)
- List.iter (fun (key, callback) -> self#addKeyBinding key callback)
- [ GdkKeysyms._F3,
- toggle_win ~check:main#showProofMenuItem proof#proofWin;
- ];
- (* about win *)
- ignore (about#aboutWin#event#connect#delete (fun _ -> true));
- ignore (main#aboutMenuItem#connect#activate (fun _ ->
- about#aboutWin#show ()));
- ignore (about#aboutDismissButton#connect#clicked (fun _ ->
- about#aboutWin#misc#hide ()));
- (* menus *)
- List.iter (fun w -> w#misc#set_sensitive false)
- [ main#saveMenuItem; main#saveAsMenuItem ];
- main#helpMenu#set_right_justified true;
- (* uri choice *)
- ()
-
- method toolbar = toolbar
- method main = main
- method about = about
- method dialog = dialog
- method uriChoice = uriChoice
- method interpChoice = interpChoice
- method fileSel = fileSel
- method proof = proof
-
- 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 uriChoices = uriChoices
-
- end
-
+++ /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/
- *)
-
-(*
-class type stringListModel =
- object
- method clear: unit -> unit
- method append: string -> unit
- end
-*)
-
- (** @param fname name of the Glade file describing the GUI *)
-class gui :
- string ->
- object
-
- method setQuitCallback : (unit -> unit) -> unit
-
- method uriChoices: MathitaGtkMisc.stringListModel
-
- (** {2 Access to low-level GTK widgets} *)
-
- method about : MathitaGeneratedGui.aboutWin
- method dialog : MathitaGeneratedGui.genericDialog
- method fileSel : MathitaGeneratedGui.fileSelectionWin
- method interpChoice : MathitaGeneratedGui.interpChoiceDialog
- method main : MathitaGeneratedGui.mainWin
- method proof : MathitaGeneratedGui.proofWin
- method toolbar : MathitaGeneratedGui.toolBarWin
- method uriChoice : MathitaGeneratedGui.uriChoiceDialog
-
- end
-
--- /dev/null
+Makefile
+buildTimeConf.ml
+config.status
+configure
+config.log
+autom4te.cache
+matita
+matita.opt
+*.cm[aiox]
+*.cmxa
+*.[ao]
--- /dev/null
+matitaGeneratedGui.cmo: matitaGeneratedGui.cmi
+matitaGeneratedGui.cmx: matitaGeneratedGui.cmi
+matitaGtkMisc.cmo: matitaGtkMisc.cmi
+matitaGtkMisc.cmx: matitaGtkMisc.cmi
+matitaGui.cmo: matitaGeneratedGui.cmi matitaGtkMisc.cmi matitaGui.cmi
+matitaGui.cmx: matitaGeneratedGui.cmx matitaGtkMisc.cmx matitaGui.cmi
+matita.cmo: matitaGeneratedGui.cmi matitaGui.cmi
+matita.cmx: matitaGeneratedGui.cmx matitaGui.cmx
+matitaGui.cmi: matitaGeneratedGui.cmi matitaGtkMisc.cmi
--- /dev/null
+
+OCAMLFIND = @OCAMLFIND@
+CAMLP4O = @CAMLP4O@
+LABLGLADECC = @LABLGLADECC@
+
+REQUIRES = lablgtk2.glade helm-registry
+OCAML_FLAGS = -package "$(REQUIRES)" -pp $(CAMLP4O)
+OCAML_THREADS_FLAGS = -thread
+OCAML_DEBUG_FLAGS =
+OCAMLC = $(OCAMLFIND) ocamlc $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS)
+OCAMLOPT = $(OCAMLFIND) opt $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS)
+OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS)
+CMOS = \
+ buildTimeConf.cmo \
+ matitaGeneratedGui.cmo \
+ matitaGtkMisc.cmo \
+ matitaGui.cmo
+CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
+
+all: matita
+opt: matita.opt
+
+matita: $(CMOS) matita.ml
+ $(OCAMLC) -linkpkg -o $@ $^
+matita.opt: $(CMXS) matita.ml
+ $(OCAMLOPT) -linkpkg -o $@ $^
+
+matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade
+ $(LABLGLADECC) $< > $@
+ $(OCAMLC) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli
+
+%.cmi: %.mli
+ $(OCAMLC) -c $<
+%.cmo %.cmi: %.ml
+ $(OCAMLC) -c $<
+%.cmx: %.ml
+ $(OCAMLOPT) -c $<
+
+clean:
+ rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o matita matita.opt
+distclean: clean
+ rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
+ rm -f config.log config.status configure Makefile buildTimeConf.ml
+ rm -f matita.glade.bak matita.gladep.bak
+ rm -rf autom4te.cache/
+
+depend: matitaGeneratedGui.ml matitaGeneratedGui.mli
+ $(OCAMLDEP) *.ml *.mli > .depend
+
+include .depend
+
+.PHONY: all opt clean distclean depend
+
--- /dev/null
+AC_INIT(matita.ml)
+
+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
+
+AC_SUBST(OCAMLFIND)
+AC_SUBST(CAMLP4O)
+AC_SUBST(LABLGLADECC)
+
+AC_OUTPUT([
+ buildTimeConf.ml
+ Makefile
+])
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="matita">
+ <key name="glade_file">matita.glade</key>
+ <key name="auto_disambiguation">true</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="GtkWindow" id="MainWin">
+ <property name="visible">True</property>
+ <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>
+
+ <child>
+ <widget class="GtkVBox" id="MainWinShape">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkMenuBar" id="MainMenuBar">
+ <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="NewMenu">
+ <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="image40">
+ <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>
+
+ <child>
+ <widget class="GtkMenu" id="NewMenu_menu">
+
+ <child>
+ <widget class="GtkMenuItem" id="NewProofMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Proof or definition ...</property>
+ <property name="use_underline">True</property>
+ <accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="NewDefsMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">(Co)Inductive _definitions ...</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
+ </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="image41">
+ <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="image42">
+ <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="image43">
+ <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="GtkMenuItem" id="separator1">
+ <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="image44">
+ <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="GtkCheckMenuItem" id="ShowToolBarMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Show Button Bar</property>
+ <property name="use_underline">True</property>
+ <property name="active">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkCheckMenuItem" id="ShowProofMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Show Proof Window</property>
+ <property name="use_underline">True</property>
+ <property name="active">False</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="GtkMenuItem" id="DebugMenuItem0">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">0</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="DebugMenuItem1">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">1</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="DebugMenuItem2">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">2</property>
+ <property name="use_underline">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>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkVPaned" id="MainVPanes">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="position">450</property>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="ProofStatus">
+ <property name="visible">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>
+ <placeholder/>
+ </child>
+ </widget>
+ <packing>
+ <property name="shrink">True</property>
+ <property name="resize">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="ScrolledUserInput">
+ <property name="visible">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>
+ <placeholder/>
+ </child>
+ </widget>
+ <packing>
+ <property name="shrink">True</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>
+
+ <child>
+ <widget class="GtkStatusbar" id="MainStatusBar">
+ <property name="visible">True</property>
+ <property name="has_resize_grip">True</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="ProofWin">
+ <property name="title" translatable="yes">Matita: current proof</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">700</property>
+ <property name="default_height">525</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+
+ <child>
+ <widget class="GtkEventBox" id="ProofWinEventBox">
+ <property name="visible">True</property>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="ScrolledProof">
+ <property name="visible">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="GtkViewport" id="viewport1">
+ <property name="visible">True</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+
+ <child>
+ <placeholder/>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </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="show_fileops">True</property>
+
+ <child internal-child="cancel_button">
+ <widget class="GtkButton" id="cancel_button1">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ </child>
+
+ <child internal-child="ok_button">
+ <widget class="GtkButton" id="ok_button1">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkWindow" id="ToolBarWin">
+ <property name="width_request">130</property>
+ <property name="height_request">450</property>
+ <property name="visible">True</property>
+ <property name="title" translatable="yes">ToolBar</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">False</property>
+ <property name="destroy_with_parent">False</property>
+
+ <child>
+ <widget class="GtkEventBox" id="ToolBarEventBox">
+ <property name="visible">True</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox1">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkVButtonBox" id="vbuttonbox1">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_DEFAULT_STYLE</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkButton" id="button1">
+ <property name="width_request">120</property>
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">button1</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="button2">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">button2</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="button3">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">button3</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="button4">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">button4</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHSeparator" id="hseparator1">
+ <property name="visible">True</property>
+ </widget>
+ <packing>
+ <property name="padding">5</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <placeholder/>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkDialog" id="GenericDialog">
+ <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="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="cancelbutton1">
+ <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="response_id">-6</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="okbutton1">
+ <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="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>
+ <placeholder/>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<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="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="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>
+ <placeholder/>
+ </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="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="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="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>
+
+ <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="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="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>
+
+ <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" translatable="yes">*</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>
+
+<widget class="GtkDialog" id="InterpChoiceDialog">
+ <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="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="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="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="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="label6">
+ <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>
+ <placeholder/>
+ </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="Debug">
+ <property name="visible">True</property>
+ <property name="title" translatable="yes">dialog1</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="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="dialog-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="dialog-action_area5">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="cancelbutton2">
+ <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="response_id">-6</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="okbutton2">
+ <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="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>
+ <placeholder/>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+</glade-interface>
--- /dev/null
+<?xml version="1.0" standalone="no"?> <!--*- mode: xml -*-->
+<!DOCTYPE glade-project SYSTEM "http://glade.gnome.org/glade-project-2.0.dtd">
+
+<glade-project>
+ <name>Matita</name>
+ <program_name>matita</program_name>
+ <gnome_support>FALSE</gnome_support>
+</glade-project>
--- /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/
+ *)
+
+exception Not_implemented of string
+let not_implemented feature = raise (Not_implemented feature)
+
+ (** exceptions whose content should be presented to the user *)
+exception Failure of string
+let error s = raise (Failure s)
+
+let _ = Helm_registry.load_from "matita.conf.xml"
+let _ = GMain.Main.init ()
+let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file")
+
+let interactive_user_uri_choice
+ ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(nonvars_button=false) ~title ~msg
+ uris
+=
+ let only_constant_choices =
+ lazy
+ (List.filter
+ (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
+ uris)
+ in
+ if (selection_mode <> `SINGLE) &&
+ (Helm_registry.get_bool "matita.auto_disambiguation")
+ then
+ Lazy.force only_constant_choices
+ else begin
+ let win = gui#uriChoice in
+ let choices = ref [] in
+ let chosen = ref false in
+ let use_only_constants = ref false in
+ win#uriChoiceDialog#set_title title;
+ win#uriChoiceLabel#set_text msg;
+ gui#uriChoices#list_store#clear ();
+ List.iter gui#uriChoices#easy_append uris;
+ win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
+ let bye = ref (fun () -> ()) in
+ let id1 =
+ win#uriChoiceConstantsButton#connect#clicked (fun _ ->
+ use_only_constants := true;
+ !bye ())
+ in
+ let id2 =
+ win#uriChoiceAutoButton#connect#clicked (fun _ ->
+ use_only_constants := true ;
+ Helm_registry.set_bool "matita.auto_disambiguation" true;
+ !bye ())
+ in
+ let id3 =
+ win#uriChoiceSelectedButton#connect#clicked (fun _ ->
+ choices := gui#uriChoices#easy_selection ();
+ !bye ())
+ in
+ bye := (fun () ->
+ win#uriChoiceDialog#misc#hide ();
+ win#uriChoiceConstantsButton#misc#disconnect id1;
+ win#uriChoiceAutoButton#misc#disconnect id2;
+ win#uriChoiceSelectedButton#misc#disconnect id3;
+ prerr_endline "quit";
+ GMain.Main.quit ());
+ win#uriChoiceDialog#show ();
+ GtkThread.main ();
+ if !use_only_constants then
+ Lazy.force only_constant_choices
+ else
+ match !choices with
+ | [] -> error "No choice"
+ | choices -> choices
+ end
+
+(*
+module DisambiguateCallbacks =
+ struct
+ let interactive_user_uri_choice =
+ assert false (* TODO *)
+(* interactive_user_uri_choice *)
+ let interactive_interpretation_choice choices =
+ assert false (* TODO *)
+ let input_or_locate_uri ~title =
+ assert false (* TODO *)
+ end
+*)
+
+let debugDialog () =
+ let dialog =
+ new MatitaGeneratedGui.debug
+ ~file:(Helm_registry.get "matita.glade_file") ()
+ in
+ let retval = ref None in
+ let return v =
+ retval := Some v;
+ dialog#debug#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (dialog#debug#event#connect#delete (fun _ -> true));
+ ignore (dialog#okbutton2#connect#clicked (fun _ -> return 1));
+ ignore (dialog#cancelbutton2#connect#clicked (fun _ -> return 2));
+ dialog#debug#show ();
+ GtkThread.main ();
+ (match !retval with None -> assert false | Some v -> v)
+
+let _ =
+ gui#main#debugMenuItem2#connect#activate (fun _ ->
+ prerr_endline (string_of_int (debugDialog ())))
+
+ (** quit program, possibly asking for confirmation *)
+let quit () = GMain.Main.quit ()
+let _ = gui#setQuitCallback quit
+let _ =
+ gui#main#debugMenuItem0#connect#activate (fun _ ->
+ let uris =
+ interactive_user_uri_choice
+ ~selection_mode:`MULTIPLE
+ ~nonvars_button:false
+ ~title:"titolo"
+ ~msg:"messaggio"
+ ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
+ "cic:/cinque.var"]
+ in
+ List.iter prerr_endline uris; print_newline ())
+let _ =
+ gui#main#debugMenuItem1#connect#activate (fun _ ->
+ Helm_registry.set_bool "matita.auto_disambiguation"
+ (not (Helm_registry.get_bool "matita.auto_disambiguation")))
+
+let _ =
+(* gui#uriChoices#easy_append "pippo"; *)
+(* gui#uriChoices#list_store#clear (); *)
+ GtkThread.main ()
+
--- /dev/null
+(* Automatically generated from matita.glade by lablgladecc *)
+
+class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"MainWin" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel =
+ new GWindow.window (GtkWindow.Window.cast
+ (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata))
+ method toplevel = toplevel
+ val mainWin =
+ new GWindow.window (GtkWindow.Window.cast
+ (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata))
+ method mainWin = mainWin
+ val mainWinShape =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"MainWinShape" ~info:"GtkVBox" xmldata))
+ method mainWinShape = mainWinShape
+ val mainMenuBar =
+ new GMenu.menu_shell (GtkMenu.MenuBar.cast
+ (Glade.get_widget_msg ~name:"MainMenuBar" ~info:"GtkMenuBar" xmldata))
+ method mainMenuBar = mainMenuBar
+ val fileMenu =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"FileMenu" ~info:"GtkMenuItem" xmldata))
+ method fileMenu = fileMenu
+ val fileMenu_menu =
+ new GMenu.menu (GtkMenu.Menu.cast
+ (Glade.get_widget_msg ~name:"FileMenu_menu" ~info:"GtkMenu" xmldata))
+ method fileMenu_menu = fileMenu_menu
+ val newMenu =
+ new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+ (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
+ method newMenu = newMenu
+ val image40 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image40" ~info:"GtkImage" xmldata))
+ method image40 = image40
+ val newMenu_menu =
+ new GMenu.menu (GtkMenu.Menu.cast
+ (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata))
+ method newMenu_menu = newMenu_menu
+ val newProofMenuItem =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"NewProofMenuItem" ~info:"GtkMenuItem" xmldata))
+ method newProofMenuItem = newProofMenuItem
+ val newDefsMenuItem =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"NewDefsMenuItem" ~info:"GtkMenuItem" xmldata))
+ method newDefsMenuItem = newDefsMenuItem
+ val openMenuItem =
+ new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+ (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata))
+ method openMenuItem = openMenuItem
+ val image41 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image41" ~info:"GtkImage" xmldata))
+ method image41 = image41
+ val saveMenuItem =
+ new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+ (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
+ method saveMenuItem = saveMenuItem
+ val image42 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image42" ~info:"GtkImage" xmldata))
+ method image42 = image42
+ val saveAsMenuItem =
+ new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+ (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
+ method saveAsMenuItem = saveAsMenuItem
+ val image43 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image43" ~info:"GtkImage" xmldata))
+ method image43 = image43
+ val separator1 =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"separator1" ~info:"GtkMenuItem" xmldata))
+ method separator1 = separator1
+ val quitMenuItem =
+ new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+ (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata))
+ method quitMenuItem = quitMenuItem
+ val image44 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image44" ~info:"GtkImage" xmldata))
+ method image44 = image44
+ val editMenu =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))
+ method editMenu = editMenu
+ val viewMenu =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"ViewMenu" ~info:"GtkMenuItem" xmldata))
+ method viewMenu = viewMenu
+ val viewMenu_menu =
+ new GMenu.menu (GtkMenu.Menu.cast
+ (Glade.get_widget_msg ~name:"ViewMenu_menu" ~info:"GtkMenu" xmldata))
+ method viewMenu_menu = viewMenu_menu
+ val showToolBarMenuItem =
+ new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
+ (Glade.get_widget_msg ~name:"ShowToolBarMenuItem" ~info:"GtkCheckMenuItem" xmldata))
+ method showToolBarMenuItem = showToolBarMenuItem
+ val showProofMenuItem =
+ new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
+ (Glade.get_widget_msg ~name:"ShowProofMenuItem" ~info:"GtkCheckMenuItem" xmldata))
+ method showProofMenuItem = showProofMenuItem
+ val debugMenu =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata))
+ method debugMenu = debugMenu
+ val debugMenu_menu =
+ new GMenu.menu (GtkMenu.Menu.cast
+ (Glade.get_widget_msg ~name:"DebugMenu_menu" ~info:"GtkMenu" xmldata))
+ method debugMenu_menu = debugMenu_menu
+ val debugMenuItem0 =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"DebugMenuItem0" ~info:"GtkMenuItem" xmldata))
+ method debugMenuItem0 = debugMenuItem0
+ val debugMenuItem1 =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"DebugMenuItem1" ~info:"GtkMenuItem" xmldata))
+ method debugMenuItem1 = debugMenuItem1
+ val debugMenuItem2 =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"DebugMenuItem2" ~info:"GtkMenuItem" xmldata))
+ method debugMenuItem2 = debugMenuItem2
+ val helpMenu =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"HelpMenu" ~info:"GtkMenuItem" xmldata))
+ method helpMenu = helpMenu
+ val helpMenu_menu =
+ new GMenu.menu (GtkMenu.Menu.cast
+ (Glade.get_widget_msg ~name:"HelpMenu_menu" ~info:"GtkMenu" xmldata))
+ method helpMenu_menu = helpMenu_menu
+ val aboutMenuItem =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"AboutMenuItem" ~info:"GtkMenuItem" xmldata))
+ method aboutMenuItem = aboutMenuItem
+ val mainVPanes =
+ new GPack.paned (GtkPack.Paned.cast
+ (Glade.get_widget_msg ~name:"MainVPanes" ~info:"GtkVPaned" xmldata))
+ method mainVPanes = mainVPanes
+ val proofStatus =
+ new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+ (Glade.get_widget_msg ~name:"ProofStatus" ~info:"GtkScrolledWindow" xmldata))
+ method proofStatus = proofStatus
+ val scrolledUserInput =
+ new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+ (Glade.get_widget_msg ~name:"ScrolledUserInput" ~info:"GtkScrolledWindow" xmldata))
+ method scrolledUserInput = scrolledUserInput
+ val mainStatusBar =
+ new GMisc.statusbar (GtkMisc.Statusbar.cast
+ (Glade.get_widget_msg ~name:"MainStatusBar" ~info:"GtkStatusbar" xmldata))
+ method mainStatusBar = mainStatusBar
+ method reparent parent =
+ mainWinShape#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+class proofWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"ProofWin" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel =
+ new GWindow.window (GtkWindow.Window.cast
+ (Glade.get_widget_msg ~name:"ProofWin" ~info:"GtkWindow" xmldata))
+ method toplevel = toplevel
+ val proofWin =
+ new GWindow.window (GtkWindow.Window.cast
+ (Glade.get_widget_msg ~name:"ProofWin" ~info:"GtkWindow" xmldata))
+ method proofWin = proofWin
+ val proofWinEventBox =
+ new GBin.event_box (GtkBin.EventBox.cast
+ (Glade.get_widget_msg ~name:"ProofWinEventBox" ~info:"GtkEventBox" xmldata))
+ method proofWinEventBox = proofWinEventBox
+ val scrolledProof =
+ new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+ (Glade.get_widget_msg ~name:"ScrolledProof" ~info:"GtkScrolledWindow" xmldata))
+ method scrolledProof = scrolledProof
+ val viewport1 =
+ new GBin.viewport (GtkBin.Viewport.cast
+ (Glade.get_widget_msg ~name:"viewport1" ~info:"GtkViewport" xmldata))
+ method viewport1 = viewport1
+ method reparent parent =
+ proofWinEventBox#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+class fileSelectionWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"FileSelectionWin" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel =
+ new GWindow.file_selection (GtkWindow.FileSelection.cast
+ (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata))
+ method toplevel = toplevel
+ val fileSelectionWin =
+ new GWindow.file_selection (GtkWindow.FileSelection.cast
+ (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata))
+ method fileSelectionWin = fileSelectionWin
+ val cancel_button1 =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"cancel_button1" ~info:"GtkButton" xmldata))
+ method cancel_button1 = cancel_button1
+ val ok_button1 =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"ok_button1" ~info:"GtkButton" xmldata))
+ method ok_button1 = ok_button1
+ method check_widgets () = ()
+ end
+class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"ToolBarWin" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel =
+ new GWindow.window (GtkWindow.Window.cast
+ (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata))
+ method toplevel = toplevel
+ val toolBarWin =
+ new GWindow.window (GtkWindow.Window.cast
+ (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata))
+ method toolBarWin = toolBarWin
+ val toolBarEventBox =
+ new GBin.event_box (GtkBin.EventBox.cast
+ (Glade.get_widget_msg ~name:"ToolBarEventBox" ~info:"GtkEventBox" xmldata))
+ method toolBarEventBox = toolBarEventBox
+ val vbox1 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"vbox1" ~info:"GtkVBox" xmldata))
+ method vbox1 = vbox1
+ val button1 =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"button1" ~info:"GtkButton" xmldata))
+ method button1 = button1
+ val button2 =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"button2" ~info:"GtkButton" xmldata))
+ method button2 = button2
+ val button3 =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"button3" ~info:"GtkButton" xmldata))
+ method button3 = button3
+ val button4 =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"button4" ~info:"GtkButton" xmldata))
+ method button4 = button4
+ method reparent parent =
+ toolBarEventBox#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+class genericDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"GenericDialog" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ new GWindow.dialog (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"GenericDialog" ~info:"GtkDialog" xmldata))
+ method toplevel = toplevel
+ val genericDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ new GWindow.dialog (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"GenericDialog" ~info:"GtkDialog" xmldata))
+ method genericDialog = genericDialog
+ val dialog_vbox1 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"dialog-vbox1" ~info:"GtkVBox" xmldata))
+ method dialog_vbox1 = dialog_vbox1
+ val cancelbutton1 =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"cancelbutton1" ~info:"GtkButton" xmldata))
+ method cancelbutton1 = cancelbutton1
+ val okbutton1 =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"okbutton1" ~info:"GtkButton" xmldata))
+ method okbutton1 = okbutton1
+ method reparent parent =
+ dialog_vbox1#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+class aboutWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"AboutWin" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ new GWindow.dialog (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"AboutWin" ~info:"GtkDialog" xmldata))
+ method toplevel = toplevel
+ val aboutWin : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ new GWindow.dialog (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"AboutWin" ~info:"GtkDialog" xmldata))
+ method aboutWin = aboutWin
+ val dialog_vbox2 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"dialog-vbox2" ~info:"GtkVBox" xmldata))
+ method dialog_vbox2 = dialog_vbox2
+ val aboutDismissButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"AboutDismissButton" ~info:"GtkButton" xmldata))
+ method aboutDismissButton = aboutDismissButton
+ method reparent parent =
+ dialog_vbox2#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+class uriChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"UriChoiceDialog" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ new GWindow.dialog (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata))
+ method toplevel = toplevel
+ val uriChoiceDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ new GWindow.dialog (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata))
+ method uriChoiceDialog = uriChoiceDialog
+ val dialog_vbox3 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"dialog-vbox3" ~info:"GtkVBox" xmldata))
+ method dialog_vbox3 = dialog_vbox3
+ val uriChoiceAbortButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"UriChoiceAbortButton" ~info:"GtkButton" xmldata))
+ method uriChoiceAbortButton = uriChoiceAbortButton
+ val uriChoiceSelectedButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"UriChoiceSelectedButton" ~info:"GtkButton" xmldata))
+ method uriChoiceSelectedButton = uriChoiceSelectedButton
+ val alignment2 =
+ new GBin.alignment (GtkBin.Alignment.cast
+ (Glade.get_widget_msg ~name:"alignment2" ~info:"GtkAlignment" xmldata))
+ method alignment2 = alignment2
+ val hbox3 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"hbox3" ~info:"GtkHBox" xmldata))
+ method hbox3 = hbox3
+ val image19 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image19" ~info:"GtkImage" xmldata))
+ method image19 = image19
+ val label3 =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"label3" ~info:"GtkLabel" xmldata))
+ method label3 = label3
+ val uriChoiceConstantsButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"UriChoiceConstantsButton" ~info:"GtkButton" xmldata))
+ method uriChoiceConstantsButton = uriChoiceConstantsButton
+ val uriChoiceAutoButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"UriChoiceAutoButton" ~info:"GtkButton" xmldata))
+ method uriChoiceAutoButton = uriChoiceAutoButton
+ val alignment1 =
+ new GBin.alignment (GtkBin.Alignment.cast
+ (Glade.get_widget_msg ~name:"alignment1" ~info:"GtkAlignment" xmldata))
+ method alignment1 = alignment1
+ val hbox1 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"hbox1" ~info:"GtkHBox" xmldata))
+ method hbox1 = hbox1
+ val image18 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image18" ~info:"GtkImage" xmldata))
+ method image18 = image18
+ val label1 =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"label1" ~info:"GtkLabel" xmldata))
+ method label1 = label1
+ val vbox2 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"vbox2" ~info:"GtkVBox" xmldata))
+ method vbox2 = vbox2
+ val uriChoiceLabel =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"UriChoiceLabel" ~info:"GtkLabel" xmldata))
+ method uriChoiceLabel = uriChoiceLabel
+ val scrolledwindow1 =
+ new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+ (Glade.get_widget_msg ~name:"scrolledwindow1" ~info:"GtkScrolledWindow" xmldata))
+ method scrolledwindow1 = scrolledwindow1
+ val uriChoiceTreeView =
+ new GTree.view (GtkTree.TreeView.cast
+ (Glade.get_widget_msg ~name:"UriChoiceTreeView" ~info:"GtkTreeView" xmldata))
+ method uriChoiceTreeView = uriChoiceTreeView
+ val hbox2 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"hbox2" ~info:"GtkHBox" xmldata))
+ method hbox2 = hbox2
+ val label2 =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"label2" ~info:"GtkLabel" xmldata))
+ method label2 = label2
+ val entry1 =
+ new GEdit.entry (GtkEdit.Entry.cast
+ (Glade.get_widget_msg ~name:"entry1" ~info:"GtkEntry" xmldata))
+ method entry1 = entry1
+ method reparent parent =
+ dialog_vbox3#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"InterpChoiceDialog" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ new GWindow.dialog (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"InterpChoiceDialog" ~info:"GtkDialog" xmldata))
+ method toplevel = toplevel
+ val interpChoiceDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ new GWindow.dialog (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"InterpChoiceDialog" ~info:"GtkDialog" xmldata))
+ method interpChoiceDialog = interpChoiceDialog
+ val dialog_vbox4 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"dialog-vbox4" ~info:"GtkVBox" xmldata))
+ method dialog_vbox4 = dialog_vbox4
+ val interpChoiceHelpButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"InterpChoiceHelpButton" ~info:"GtkButton" xmldata))
+ method interpChoiceHelpButton = interpChoiceHelpButton
+ val interpChoiceCancelButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"InterpChoiceCancelButton" ~info:"GtkButton" xmldata))
+ method interpChoiceCancelButton = interpChoiceCancelButton
+ val interpChoiceOkButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"InterpChoiceOkButton" ~info:"GtkButton" xmldata))
+ method interpChoiceOkButton = interpChoiceOkButton
+ val vbox3 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"vbox3" ~info:"GtkVBox" xmldata))
+ method vbox3 = vbox3
+ val label6 =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"label6" ~info:"GtkLabel" xmldata))
+ method label6 = label6
+ method reparent parent =
+ dialog_vbox4#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+class debug ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"Debug" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ new GWindow.dialog (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata))
+ method toplevel = toplevel
+ val debug : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ new GWindow.dialog (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata))
+ method debug = debug
+ val dialog_vbox5 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"dialog-vbox5" ~info:"GtkVBox" xmldata))
+ method dialog_vbox5 = dialog_vbox5
+ val cancelbutton2 =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"cancelbutton2" ~info:"GtkButton" xmldata))
+ method cancelbutton2 = cancelbutton2
+ val okbutton2 =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"okbutton2" ~info:"GtkButton" xmldata))
+ method okbutton2 = okbutton2
+ method reparent parent =
+ dialog_vbox5#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+
+let check_all ?(show=false) () =
+ ignore (GMain.Main.init ());
+ let debug = new debug () in
+ if show then debug#toplevel#show ();
+ debug#check_widgets ();
+ let interpChoiceDialog = new interpChoiceDialog () in
+ if show then interpChoiceDialog#toplevel#show ();
+ interpChoiceDialog#check_widgets ();
+ let uriChoiceDialog = new uriChoiceDialog () in
+ if show then uriChoiceDialog#toplevel#show ();
+ uriChoiceDialog#check_widgets ();
+ let aboutWin = new aboutWin () in
+ if show then aboutWin#toplevel#show ();
+ aboutWin#check_widgets ();
+ let genericDialog = new genericDialog () in
+ if show then genericDialog#toplevel#show ();
+ genericDialog#check_widgets ();
+ let toolBarWin = new toolBarWin () in
+ if show then toolBarWin#toplevel#show ();
+ toolBarWin#check_widgets ();
+ let fileSelectionWin = new fileSelectionWin () in
+ if show then fileSelectionWin#toplevel#show ();
+ fileSelectionWin#check_widgets ();
+ let proofWin = new proofWin () in
+ if show then proofWin#toplevel#show ();
+ proofWin#check_widgets ();
+ let mainWin = new mainWin () in
+ if show then mainWin#toplevel#show ();
+ mainWin#check_widgets ();
+ if show then GMain.Main.main ()
+;;
--- /dev/null
+class mainWin :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val aboutMenuItem : GMenu.menu_item
+ val debugMenu : GMenu.menu_item
+ val debugMenuItem0 : GMenu.menu_item
+ val debugMenuItem1 : GMenu.menu_item
+ val debugMenuItem2 : GMenu.menu_item
+ val debugMenu_menu : GMenu.menu
+ val editMenu : GMenu.menu_item
+ val fileMenu : GMenu.menu_item
+ val fileMenu_menu : GMenu.menu
+ val helpMenu : GMenu.menu_item
+ val helpMenu_menu : GMenu.menu
+ val image40 : GMisc.image
+ val image41 : GMisc.image
+ val image42 : GMisc.image
+ val image43 : GMisc.image
+ val image44 : GMisc.image
+ val mainMenuBar : GMenu.menu_shell
+ val mainStatusBar : GMisc.statusbar
+ val mainVPanes : GPack.paned
+ val mainWin : GWindow.window
+ val mainWinShape : GPack.box
+ val newDefsMenuItem : GMenu.menu_item
+ val newMenu : GMenu.image_menu_item
+ val newMenu_menu : GMenu.menu
+ val newProofMenuItem : GMenu.menu_item
+ val openMenuItem : GMenu.image_menu_item
+ val proofStatus : GBin.scrolled_window
+ val quitMenuItem : GMenu.image_menu_item
+ val saveAsMenuItem : GMenu.image_menu_item
+ val saveMenuItem : GMenu.image_menu_item
+ val scrolledUserInput : GBin.scrolled_window
+ val separator1 : GMenu.menu_item
+ val showProofMenuItem : GMenu.check_menu_item
+ val showToolBarMenuItem : GMenu.check_menu_item
+ val toplevel : GWindow.window
+ val viewMenu : GMenu.menu_item
+ val viewMenu_menu : GMenu.menu
+ val xml : Glade.glade_xml Gtk.obj
+ method aboutMenuItem : GMenu.menu_item
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method check_widgets : unit -> unit
+ method debugMenu : GMenu.menu_item
+ method debugMenuItem0 : GMenu.menu_item
+ method debugMenuItem1 : GMenu.menu_item
+ method debugMenuItem2 : GMenu.menu_item
+ method debugMenu_menu : GMenu.menu
+ method editMenu : GMenu.menu_item
+ method fileMenu : GMenu.menu_item
+ method fileMenu_menu : GMenu.menu
+ method helpMenu : GMenu.menu_item
+ method helpMenu_menu : GMenu.menu
+ method image40 : GMisc.image
+ method image41 : GMisc.image
+ method image42 : GMisc.image
+ method image43 : GMisc.image
+ method image44 : GMisc.image
+ method mainMenuBar : GMenu.menu_shell
+ method mainStatusBar : GMisc.statusbar
+ method mainVPanes : GPack.paned
+ method mainWin : GWindow.window
+ method mainWinShape : GPack.box
+ method newDefsMenuItem : GMenu.menu_item
+ method newMenu : GMenu.image_menu_item
+ method newMenu_menu : GMenu.menu
+ method newProofMenuItem : GMenu.menu_item
+ method openMenuItem : GMenu.image_menu_item
+ method proofStatus : GBin.scrolled_window
+ method quitMenuItem : GMenu.image_menu_item
+ method reparent : GObj.widget -> unit
+ method saveAsMenuItem : GMenu.image_menu_item
+ method saveMenuItem : GMenu.image_menu_item
+ method scrolledUserInput : GBin.scrolled_window
+ method separator1 : GMenu.menu_item
+ method showProofMenuItem : GMenu.check_menu_item
+ method showToolBarMenuItem : GMenu.check_menu_item
+ method toplevel : GWindow.window
+ method viewMenu : GMenu.menu_item
+ method viewMenu_menu : GMenu.menu
+ method xml : Glade.glade_xml Gtk.obj
+ end
+class proofWin :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val proofWin : GWindow.window
+ val proofWinEventBox : GBin.event_box
+ val scrolledProof : GBin.scrolled_window
+ val toplevel : GWindow.window
+ val viewport1 : GBin.viewport
+ val xml : Glade.glade_xml Gtk.obj
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method check_widgets : unit -> unit
+ method proofWin : GWindow.window
+ method proofWinEventBox : GBin.event_box
+ method reparent : GObj.widget -> unit
+ method scrolledProof : GBin.scrolled_window
+ method toplevel : GWindow.window
+ method viewport1 : GBin.viewport
+ method xml : Glade.glade_xml Gtk.obj
+ end
+class fileSelectionWin :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val cancel_button1 : GButton.button
+ val fileSelectionWin : GWindow.file_selection
+ val ok_button1 : GButton.button
+ val toplevel : GWindow.file_selection
+ val xml : Glade.glade_xml Gtk.obj
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method cancel_button1 : GButton.button
+ method check_widgets : unit -> unit
+ method fileSelectionWin : GWindow.file_selection
+ method ok_button1 : GButton.button
+ method toplevel : GWindow.file_selection
+ method xml : Glade.glade_xml Gtk.obj
+ end
+class toolBarWin :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val button1 : GButton.button
+ val button2 : GButton.button
+ val button3 : GButton.button
+ val button4 : GButton.button
+ val toolBarEventBox : GBin.event_box
+ val toolBarWin : GWindow.window
+ val toplevel : GWindow.window
+ val vbox1 : GPack.box
+ val xml : Glade.glade_xml Gtk.obj
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method button1 : GButton.button
+ method button2 : GButton.button
+ method button3 : GButton.button
+ method button4 : GButton.button
+ method check_widgets : unit -> unit
+ method reparent : GObj.widget -> unit
+ method toolBarEventBox : GBin.event_box
+ method toolBarWin : GWindow.window
+ method toplevel : GWindow.window
+ method vbox1 : GPack.box
+ method xml : Glade.glade_xml Gtk.obj
+ end
+class genericDialog :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val cancelbutton1 : GButton.button
+ val dialog_vbox1 : GPack.box
+ val genericDialog : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val okbutton1 : GButton.button
+ val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val xml : Glade.glade_xml Gtk.obj
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method cancelbutton1 : GButton.button
+ method check_widgets : unit -> unit
+ method dialog_vbox1 : GPack.box
+ method genericDialog :
+ [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method okbutton1 : GButton.button
+ method reparent : GObj.widget -> unit
+ method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method xml : Glade.glade_xml Gtk.obj
+ end
+class aboutWin :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val aboutDismissButton : GButton.button
+ val aboutWin : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val dialog_vbox2 : GPack.box
+ val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val xml : Glade.glade_xml Gtk.obj
+ method aboutDismissButton : GButton.button
+ method aboutWin : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method check_widgets : unit -> unit
+ method dialog_vbox2 : GPack.box
+ method reparent : GObj.widget -> unit
+ method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method xml : Glade.glade_xml Gtk.obj
+ end
+class uriChoiceDialog :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val alignment1 : GBin.alignment
+ val alignment2 : GBin.alignment
+ val dialog_vbox3 : GPack.box
+ val entry1 : GEdit.entry
+ val hbox1 : GPack.box
+ val hbox2 : GPack.box
+ val hbox3 : GPack.box
+ val image18 : GMisc.image
+ val image19 : GMisc.image
+ val label1 : GMisc.label
+ val label2 : GMisc.label
+ val label3 : GMisc.label
+ val scrolledwindow1 : GBin.scrolled_window
+ val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val uriChoiceAbortButton : GButton.button
+ val uriChoiceAutoButton : GButton.button
+ val uriChoiceConstantsButton : GButton.button
+ val uriChoiceDialog :
+ [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val uriChoiceLabel : GMisc.label
+ val uriChoiceSelectedButton : GButton.button
+ val uriChoiceTreeView : GTree.view
+ val vbox2 : GPack.box
+ val xml : Glade.glade_xml Gtk.obj
+ method alignment1 : GBin.alignment
+ method alignment2 : GBin.alignment
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method check_widgets : unit -> unit
+ method dialog_vbox3 : GPack.box
+ method entry1 : GEdit.entry
+ method hbox1 : GPack.box
+ method hbox2 : GPack.box
+ method hbox3 : GPack.box
+ method image18 : GMisc.image
+ method image19 : GMisc.image
+ method label1 : GMisc.label
+ method label2 : GMisc.label
+ method label3 : GMisc.label
+ method reparent : GObj.widget -> unit
+ method scrolledwindow1 : GBin.scrolled_window
+ method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method uriChoiceAbortButton : GButton.button
+ method uriChoiceAutoButton : GButton.button
+ method uriChoiceConstantsButton : GButton.button
+ method uriChoiceDialog :
+ [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method uriChoiceLabel : GMisc.label
+ method uriChoiceSelectedButton : GButton.button
+ method uriChoiceTreeView : GTree.view
+ method vbox2 : GPack.box
+ method xml : Glade.glade_xml Gtk.obj
+ end
+class interpChoiceDialog :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val dialog_vbox4 : GPack.box
+ val interpChoiceCancelButton : GButton.button
+ val interpChoiceDialog :
+ [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val interpChoiceHelpButton : GButton.button
+ val interpChoiceOkButton : GButton.button
+ val label6 : GMisc.label
+ val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val vbox3 : GPack.box
+ val xml : Glade.glade_xml Gtk.obj
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method check_widgets : unit -> unit
+ method dialog_vbox4 : GPack.box
+ method interpChoiceCancelButton : GButton.button
+ method interpChoiceDialog :
+ [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method interpChoiceHelpButton : GButton.button
+ method interpChoiceOkButton : GButton.button
+ method label6 : GMisc.label
+ method reparent : GObj.widget -> unit
+ method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method vbox3 : GPack.box
+ method xml : Glade.glade_xml Gtk.obj
+ end
+class debug :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val cancelbutton2 : GButton.button
+ val debug : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val dialog_vbox5 : GPack.box
+ val okbutton2 : GButton.button
+ val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val xml : Glade.glade_xml Gtk.obj
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method cancelbutton2 : GButton.button
+ method check_widgets : unit -> unit
+ method debug : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method dialog_vbox5 : GPack.box
+ method okbutton2 : GButton.button
+ method reparent : GObj.widget -> unit
+ method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method xml : Glade.glade_xml Gtk.obj
+ end
+val check_all : ?show:bool -> unit -> unit
--- /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 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
+
--- /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/
+ *)
+
+(** {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
+
+ (** 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
+
--- /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/
+ *)
+
+(*
+class stringListModel' uriChoiceDialog =
+ let tree_view = uriChoiceDialog#uriChoiceTreeView in
+ 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
+ let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in
+ let view_column = GTree.view_column ~renderer () in
+ let _ = tree_view#set_model (Some (list_store :> GTree.model)) in
+ let _ = tree_view#append_column view_column in
+ object
+ method append s =
+ let tree_iter = list_store#append () in
+ list_store#set ~row:tree_iter ~column:text_column s
+ method clear () = list_store#clear ()
+ end
+*)
+
+open MatitaGeneratedGui
+open MatitaGtkMisc
+
+class gui file =
+ (* creation order _is_ relevant for windows placement *)
+ let toolbar = new toolBarWin ~file () in
+ let main = new mainWin ~file () in
+ let about = new aboutWin ~file () in
+ let dialog = new genericDialog ~file () in
+ let uriChoice = new uriChoiceDialog ~file () in
+ let interpChoice = new interpChoiceDialog ~file () in
+ let fileSel = new fileSelectionWin ~file () in
+ let proof = new proofWin ~file () in
+ let keyBindingBoxes = (* event boxes which should receive global key events *)
+ [ toolbar#toolBarEventBox; proof#proofWinEventBox ]
+ in
+ let uriChoices = new stringListModel uriChoice#uriChoiceTreeView in
+ object (self)
+ initializer
+ (* glade's check widgets *)
+ List.iter (fun w -> w#check_widgets ())
+ (let c w = (w :> <check_widgets: unit -> unit>) in
+ [ c about; c dialog; c fileSel; c main; c proof; c toolbar;
+ c uriChoice; c interpChoice ]);
+ (* show/hide commands *)
+ toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
+ toggle_visibility proof#proofWin main#showProofMenuItem;
+ (* "global" key bindings *)
+ List.iter (fun (key, callback) -> self#addKeyBinding key callback)
+ [ GdkKeysyms._F3,
+ toggle_win ~check:main#showProofMenuItem proof#proofWin;
+ ];
+ (* about win *)
+ ignore (about#aboutWin#event#connect#delete (fun _ -> true));
+ ignore (main#aboutMenuItem#connect#activate (fun _ ->
+ about#aboutWin#show ()));
+ ignore (about#aboutDismissButton#connect#clicked (fun _ ->
+ about#aboutWin#misc#hide ()));
+ (* menus *)
+ List.iter (fun w -> w#misc#set_sensitive false)
+ [ main#saveMenuItem; main#saveAsMenuItem ];
+ main#helpMenu#set_right_justified true;
+ (* uri choice *)
+ ()
+
+ method toolbar = toolbar
+ method main = main
+ method about = about
+ method dialog = dialog
+ method uriChoice = uriChoice
+ method interpChoice = interpChoice
+ method fileSel = fileSel
+ method proof = proof
+
+ 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 uriChoices = uriChoices
+
+ end
+
--- /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/
+ *)
+
+(*
+class type stringListModel =
+ object
+ method clear: unit -> unit
+ method append: string -> unit
+ end
+*)
+
+ (** @param fname name of the Glade file describing the GUI *)
+class gui :
+ string ->
+ object
+
+ method setQuitCallback : (unit -> unit) -> unit
+
+ method uriChoices: MatitaGtkMisc.stringListModel
+
+ (** {2 Access to low-level GTK widgets} *)
+
+ method about : MatitaGeneratedGui.aboutWin
+ method dialog : MatitaGeneratedGui.genericDialog
+ method fileSel : MatitaGeneratedGui.fileSelectionWin
+ method interpChoice : MatitaGeneratedGui.interpChoiceDialog
+ method main : MatitaGeneratedGui.mainWin
+ method proof : MatitaGeneratedGui.proofWin
+ method toolbar : MatitaGeneratedGui.toolBarWin
+ method uriChoice : MatitaGeneratedGui.uriChoiceDialog
+
+ end
+
projects / helm.git / commitdiff