<glade-interface>
-<widget class="GtkWindow" id="MainWin">
- <property name="title" translatable="yes">Matita</property>
+<widget class="GtkDialog" id="AboutWin">
+ <property name="title" translatable="yes">Matita: about</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_CENTER</property>
+ <property name="modal">True</property>
+ <property name="resizable">False</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="dialog-vbox2">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="dialog-action_area2">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="AboutDismissButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-ok</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-5</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="AboutLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes"><b>Matita @VERSION@</b>
+
+<tt>http://helm.cs.unibo.it</tt>
+
+Copyright (C) 2004,
+<i>the HELM team</i></property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">True</property>
+ <property name="justify">GTK_JUSTIFY_CENTER</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">5</property>
+ <property name="ypad">5</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkWindow" id="BrowserWin">
+ <property name="width_request">400</property>
+ <property name="height_request">500</property>
+ <property name="visible">True</property>
+ <property name="title" translatable="yes">Cic browser</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
<property name="window_position">GTK_WIN_POS_NONE</property>
<property name="modal">False</property>
- <property name="default_width">800</property>
- <property name="default_height">600</property>
<property name="resizable">True</property>
<property name="destroy_with_parent">False</property>
<property name="decorated">True</property>
<property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
<child>
- <widget class="GtkEventBox" id="MainWinEventBox">
+ <widget class="GtkEventBox" id="BrowserWinEventBox">
<property name="visible">True</property>
<property name="visible_window">True</property>
<property name="above_child">False</property>
<child>
- <widget class="GtkVBox" id="MainWinShape">
+ <widget class="GtkVBox" id="BrowserVBox">
<property name="visible">True</property>
<property name="homogeneous">False</property>
<property name="spacing">0</property>
<child>
- <widget class="GtkMenuBar" id="MainMenuBar">
+ <widget class="GtkHandleBox" id="handlebox1">
<property name="visible">True</property>
+ <property name="shadow_type">GTK_SHADOW_OUT</property>
+ <property name="handle_position">GTK_POS_LEFT</property>
+ <property name="snap_edge">GTK_POS_TOP</property>
<child>
- <widget class="GtkMenuItem" id="FileMenu">
+ <widget class="GtkHBox" id="hbox7">
<property name="visible">True</property>
- <property name="label" translatable="yes">_File</property>
- <property name="use_underline">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
<child>
- <widget class="GtkMenu" id="FileMenu_menu">
+ <widget class="GtkButton" id="BrowserNewButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">new browser win</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<child>
- <widget class="GtkImageMenuItem" id="NewMenu">
+ <widget class="GtkImage" id="image191">
<property name="visible">True</property>
- <property name="label" translatable="yes">_New</property>
- <property name="use_underline">True</property>
+ <property name="stock">gtk-new</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
- <child internal-child="image">
- <widget class="GtkImage" id="image224">
- <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="GtkButton" id="BrowserBackButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">history back</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkAlignment" id="alignment3">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xscale">0</property>
+ <property name="yscale">0</property>
+ <property name="top_padding">0</property>
+ <property name="bottom_padding">0</property>
+ <property name="left_padding">0</property>
+ <property name="right_padding">0</property>
<child>
- <widget class="GtkMenu" id="NewMenu_menu">
+ <widget class="GtkHBox" id="hbox6">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
<child>
- <widget class="GtkMenuItem" id="NewProofMenuItem">
+ <widget class="GtkImage" id="image188">
<property name="visible">True</property>
- <property name="label" translatable="yes">_Proof or definition ...</property>
- <property name="use_underline">True</property>
+ <property name="stock">gtk-go-back</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</child>
<child>
- <widget class="GtkMenuItem" id="NewDefsMenuItem">
+ <widget class="GtkLabel" id="label10">
<property name="visible">True</property>
- <property name="label" translatable="yes">(Co)Inductive _definitions ...</property>
+ <property name="label" translatable="yes"></property>
<property name="use_underline">True</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</child>
</widget>
</child>
</widget>
</child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="BrowserForwardButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">history forward</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<child>
- <widget class="GtkImageMenuItem" id="OpenMenuItem">
+ <widget class="GtkImage" id="image189">
<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="image225">
- <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>
+ <property name="stock">gtk-go-forward</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
</widget>
</child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="BrowserRefreshButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">refresh</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<child>
- <widget class="GtkImageMenuItem" id="SaveMenuItem">
+ <widget class="GtkImage" id="image229">
<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="image226">
- <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="image227">
- <property name="visible">True</property>
- <property name="stock">gtk-save-as</property>
- <property name="icon_size">1</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- </child>
- </widget>
- </child>
-
- <child>
- <widget class="GtkSeparatorMenuItem" id="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="image228">
- <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>
+ <property name="stock">gtk-refresh</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
</widget>
</child>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</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="GtkMenuItem" id="NewCicBrowserMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">New Cic Browser</property>
- <property name="use_underline">True</property>
- <accelerator key="F3" modifiers="0" signal="activate"/>
- </widget>
- </child>
-
- <child>
- <widget class="GtkCheckMenuItem" id="ShowScriptMenuItem">
- <property name="visible">True</property>
- <property name="label" translatable="yes">Show Script Window</property>
- <property name="use_underline">True</property>
- <property name="active">False</property>
- <accelerator key="F5" modifiers="0" signal="activate"/>
- </widget>
- </child>
-
- <child>
- <widget class="GtkSeparatorMenuItem" id="separator3">
- <property name="visible">True</property>
- </widget>
- </child>
+ <widget class="GtkButton" id="BrowserHomeButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">home</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
<child>
- <widget class="GtkMenuItem" id="ShowConsoleMenuItem">
+ <widget class="GtkImage" id="image190">
<property name="visible">True</property>
- <property name="label" translatable="yes">Toggle console</property>
- <property name="use_underline">True</property>
- <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+ <property name="stock">gtk-home</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
</widget>
</child>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</child>
- </widget>
- </child>
-
- <child>
- <widget class="GtkMenuItem" id="DebugMenu">
- <property name="visible">True</property>
- <property name="label" translatable="yes">Debug</property>
- <property name="use_underline">True</property>
<child>
- <widget class="GtkMenu" id="DebugMenu_menu">
-
- <child>
- <widget class="GtkSeparatorMenuItem" id="separator2">
- <property name="visible">True</property>
- </widget>
- </child>
+ <widget class="GtkImage" id="image187">
+ <property name="visible">True</property>
+ <property name="stock">gtk-jump-to</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
</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 class="GtkEntry" id="BrowserUri">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">cic uri</property>
+ <property name="can_focus">True</property>
+ <property name="editable">True</property>
+ <property name="visibility">True</property>
+ <property name="max_length">0</property>
+ <property name="text" translatable="yes"></property>
+ <property name="has_frame">True</property>
+ <property name="invisible_char">*</property>
+ <property name="activates_default">False</property>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
</child>
</widget>
</child>
<packing>
<property name="padding">0</property>
<property name="expand">False</property>
- <property name="fill">False</property>
+ <property name="fill">True</property>
</packing>
</child>
<child>
- <widget class="GtkVPaned" id="MainVPanes">
+ <widget class="GtkFrame" id="frame1">
<property name="visible">True</property>
- <property name="can_focus">True</property>
- <property name="position">450</property>
+ <property name="label_xalign">0</property>
+ <property name="label_yalign">0</property>
+ <property name="shadow_type">GTK_SHADOW_NONE</property>
<child>
- <widget class="GtkNotebook" id="SequentsNotebook">
+ <widget class="GtkScrolledWindow" id="ScrolledBrowser">
<property name="visible">True</property>
<property name="can_focus">True</property>
- <property name="show_tabs">True</property>
- <property name="show_border">True</property>
- <property name="tab_pos">GTK_POS_TOP</property>
- <property name="scrollable">False</property>
- <property name="enable_popup">False</property>
- </widget>
- <packing>
- <property name="shrink">True</property>
- <property name="resize">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkEventBox" id="ConsoleEventBox">
- <property name="visible">True</property>
- <property name="visible_window">True</property>
- <property name="above_child">False</property>
+ <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_NONE</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
- <widget class="GtkHBox" id="ConsoleHBox">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
+ <placeholder/>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+</widget>
- <child>
- <widget class="GtkVBox" id="vbox6">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
+<widget class="GtkDialog" id="ConfirmationDialog">
+ <property name="title" translatable="yes">DUMMY</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_CENTER</property>
+ <property name="modal">True</property>
+ <property name="resizable">False</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+ <property name="has_separator">True</property>
- <child>
- <widget class="GtkButton" id="HideConsoleButton">
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Hide console</property>
- <property name="can_focus">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">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>
- <widget class="GtkImage" id="image169">
- <property name="visible">True</property>
- <property name="stock">gtk-close</property>
- <property name="icon_size">4</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
+ <child 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="GtkScrolledWindow" id="ScrolledConsole">
- <property name="visible">True</property>
- <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
- <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
- <property name="shadow_type">GTK_SHADOW_IN</property>
- <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+ <child>
+ <widget class="GtkButton" id="ConfirmationDialogCancelButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-cancel</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-6</property>
+ </widget>
+ </child>
- <child>
- <placeholder/>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">True</property>
- <property name="fill">True</property>
- </packing>
- </child>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="shrink">True</property>
- <property name="resize">False</property>
- </packing>
- </child>
+ <child>
+ <widget class="GtkButton" id="ConfirmationDialogOkButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-ok</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-5</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="ConfirmationDialogLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">DUMMY</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_CENTER</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkDialog" id="EmptyDialog">
+ <property name="visible">True</property>
+ <property name="title" translatable="yes">DUMMY</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="EmptyDialogVBox">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="dialog-action_area5">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="EmptyDialogCancelButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-cancel</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-6</property>
</widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">True</property>
- <property name="fill">True</property>
- </packing>
</child>
<child>
- <widget class="GtkStatusbar" id="MainStatusBar">
+ <widget class="GtkButton" id="EmptyDialogOkButton">
<property name="visible">True</property>
- <property name="has_resize_grip">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-ok</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-5</property>
</widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
</child>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="EmptyDialogLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">DUMMY</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <placeholder/>
</child>
</widget>
</child>
</child>
</widget>
-<widget class="GtkWindow" id="ToolBarWin">
- <property name="width_request">155</property>
- <property name="height_request">450</property>
- <property name="title" translatable="yes">Tactics</property>
+<widget class="GtkDialog" id="InterpChoiceDialog">
+ <property name="height_request">200</property>
+ <property name="title" translatable="yes">Interpretation choice</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
<property name="window_position">GTK_WIN_POS_NONE</property>
- <property name="modal">False</property>
- <property name="resizable">False</property>
+ <property name="modal">True</property>
+ <property name="resizable">True</property>
<property name="destroy_with_parent">False</property>
<property name="decorated">True</property>
<property name="skip_taskbar_hint">False</property>
<property name="skip_pager_hint">False</property>
- <property name="type_hint">GDK_WINDOW_TYPE_HINT_TOOLBAR</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
<property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+ <property name="has_separator">True</property>
- <child>
- <widget class="GtkEventBox" id="ToolBarEventBox">
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="dialog-vbox4">
<property name="visible">True</property>
- <property name="visible_window">True</property>
- <property name="above_child">False</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
- <child>
- <widget class="GtkVBox" id="ToolBarVBox">
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="dialog-action_area4">
<property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
<child>
- <widget class="GtkToolbar" id="toolbar2">
+ <widget class="GtkButton" id="InterpChoiceHelpButton">
<property name="visible">True</property>
- <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
- <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
- <property name="tooltips">True</property>
- <property name="show_arrow">True</property>
-
- <child>
- <widget class="GtkToolItem" id="toolitem4">
- <property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
-
- <child>
- <widget class="GtkButton" id="introsButton">
- <property name="width_request">50</property>
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Intros</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">intros</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
- </child>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-help</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-11</property>
+ </widget>
+ </child>
- <child>
- <widget class="GtkToolItem" id="toolitem5">
- <property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
+ <child>
+ <widget class="GtkButton" id="InterpChoiceCancelButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-cancel</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-6</property>
+ </widget>
+ </child>
- <child>
- <widget class="GtkButton" id="applyButton">
- <property name="width_request">50</property>
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Apply</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">apply</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
- </child>
+ <child>
+ <widget class="GtkButton" id="InterpChoiceOkButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-ok</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">-5</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ <property name="pack_type">GTK_PACK_END</property>
+ </packing>
+ </child>
- <child>
- <widget class="GtkToolItem" id="toolitem6">
- <property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
+ <child>
+ <widget class="GtkVBox" id="vbox3">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
- <child>
- <widget class="GtkButton" id="exactButton">
- <property name="width_request">50</property>
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Exact</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">exact</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
- </child>
+ <child>
+ <widget class="GtkLabel" id="InterpChoiceDialogLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">some informative message here ...</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
</widget>
<packing>
<property name="padding">0</property>
</child>
<child>
- <widget class="GtkToolbar" id="toolbar3">
+ <widget class="GtkScrolledWindow" id="scrolledwindow4">
<property name="visible">True</property>
- <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
- <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
- <property name="tooltips">True</property>
- <property name="show_arrow">True</property>
-
- <child>
- <widget class="GtkToolItem" id="toolitem7">
- <property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
-
- <child>
- <widget class="GtkButton" id="elimButton">
- <property name="width_request">50</property>
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Elim</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">elim</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
- </child>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
- <widget class="GtkToolItem" id="toolitem8">
+ <widget class="GtkTreeView" id="InterpChoiceTreeView">
<property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
-
- <child>
- <widget class="GtkButton" id="elimTypeButton">
- <property name="width_request">50</property>
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">ElimType</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">elimTy</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- </widget>
- </child>
+ <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>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
</child>
</widget>
<packing>
<property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
</packing>
</child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkWindow" id="MainWin">
+ <property name="title" translatable="yes">Matita</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="default_width">800</property>
+ <property name="default_height">600</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+
+ <child>
+ <widget class="GtkEventBox" id="MainWinEventBox">
+ <property name="visible">True</property>
+ <property name="visible_window">True</property>
+ <property name="above_child">False</property>
+
+ <child>
+ <widget class="GtkVBox" id="MainWinShape">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
<child>
- <widget class="GtkToolbar" id="toolbar4">
+ <widget class="GtkMenuBar" id="MainMenuBar">
<property name="visible">True</property>
- <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
- <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
- <property name="tooltips">True</property>
- <property name="show_arrow">True</property>
<child>
- <widget class="GtkToolItem" id="toolitem9">
+ <widget class="GtkMenuItem" id="FileMenu">
<property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
-
+ <property name="label" translatable="yes">_File</property>
+ <property name="use_underline">True</property>
+
<child>
- <widget class="GtkButton" id="splitButton">
- <property name="width_request">50</property>
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Split</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">split</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
+ <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="image224">
+ <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>
+ </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="image225">
+ <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="image226">
+ <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="image227">
+ <property name="visible">True</property>
+ <property name="stock">gtk-save-as</property>
+ <property name="icon_size">1</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkSeparatorMenuItem" id="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="image228">
+ <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>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
</child>
<child>
- <widget class="GtkToolItem" id="toolitem10">
+ <widget class="GtkMenuItem" id="EditMenu">
<property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</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="GtkButton" id="leftButton">
- <property name="width_request">25</property>
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Left</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">L</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
+ <widget 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="GtkMenuItem" id="NewCicBrowserMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">New Cic Browser</property>
+ <property name="use_underline">True</property>
+ <accelerator key="F3" modifiers="0" signal="activate"/>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkCheckMenuItem" id="ShowScriptMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Show Script Window</property>
+ <property name="use_underline">True</property>
+ <property name="active">False</property>
+ <accelerator key="F5" modifiers="0" signal="activate"/>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkSeparatorMenuItem" id="separator3">
+ <property name="visible">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="ShowConsoleMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Toggle console</property>
+ <property name="use_underline">True</property>
+ <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+ </widget>
+ </child>
</widget>
</child>
</widget>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
</child>
<child>
- <widget class="GtkToolItem" id="toolitem11">
+ <widget class="GtkMenuItem" id="DebugMenu">
<property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
+ <property name="label" translatable="yes">Debug</property>
+ <property name="use_underline">True</property>
<child>
- <widget class="GtkButton" id="rightButton">
- <property name="width_request">25</property>
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Right</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">R</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
+ <widget class="GtkMenu" id="DebugMenu_menu">
+
+ <child>
+ <widget class="GtkSeparatorMenuItem" id="separator2">
+ <property name="visible">True</property>
+ </widget>
+ </child>
</widget>
</child>
</widget>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
</child>
<child>
- <widget class="GtkToolItem" id="toolitem12">
+ <widget class="GtkMenuItem" id="HelpMenu">
<property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
+ <property name="label" translatable="yes">_Help</property>
+ <property name="use_underline">True</property>
<child>
- <widget class="GtkButton" id="existsButton">
- <property name="width_request">25</property>
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Exists</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">∃</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
+ <widget 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>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
</child>
</widget>
<packing>
</child>
<child>
- <widget class="GtkToolbar" id="toolbar5">
+ <widget class="GtkVPaned" id="MainVPanes">
<property name="visible">True</property>
- <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
- <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
- <property name="tooltips">True</property>
- <property name="show_arrow">True</property>
+ <property name="can_focus">True</property>
+ <property name="position">450</property>
<child>
- <widget class="GtkToolItem" id="toolitem14">
+ <widget class="GtkNotebook" id="SequentsNotebook">
<property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
+ <property name="can_focus">True</property>
+ <property name="show_tabs">True</property>
+ <property name="show_border">True</property>
+ <property name="tab_pos">GTK_POS_TOP</property>
+ <property name="scrollable">False</property>
+ <property name="enable_popup">False</property>
+ </widget>
+ <packing>
+ <property name="shrink">True</property>
+ <property name="resize">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkEventBox" id="ConsoleEventBox">
+ <property name="visible">True</property>
+ <property name="visible_window">True</property>
+ <property name="above_child">False</property>
<child>
- <widget class="GtkButton" id="reflexivityButton">
- <property name="width_request">50</property>
+ <widget class="GtkHBox" id="ConsoleHBox">
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">Reflexivity</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">refl</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox6">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkButton" id="HideConsoleButton">
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Hide console</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image169">
+ <property name="visible">True</property>
+ <property name="stock">gtk-close</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="ScrolledConsole">
+ <property name="visible">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <placeholder/>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
</widget>
</child>
</widget>
<packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
+ <property name="shrink">True</property>
+ <property name="resize">False</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>
+ </child>
+</widget>
+
+<widget class="GtkWindow" id="ScriptWin">
+ <property name="title" translatable="yes">Matita: script</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">450</property>
+ <property name="default_height">800</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+
+ <child>
+ <widget class="GtkEventBox" id="ScriptWinEventBox">
+ <property name="visible">True</property>
+ <property name="visible_window">True</property>
+ <property name="above_child">False</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox7">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkHandleBox" id="handlebox2">
+ <property name="visible">True</property>
+ <property name="shadow_type">GTK_SHADOW_OUT</property>
+ <property name="handle_position">GTK_POS_LEFT</property>
+ <property name="snap_edge">GTK_POS_TOP</property>
<child>
- <widget class="GtkToolItem" id="toolitem15">
+ <widget class="GtkHBox" id="hbox8">
<property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
- <child>
- <widget class="GtkButton" id="symmetryButton">
- <property name="width_request">50</property>
+ <child>
+ <widget class="GtkButton" id="ScriptWinTopButton">
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">Symmetry</property>
+ <property name="tooltip" translatable="yes">restart</property>
<property name="can_focus">True</property>
- <property name="label" translatable="yes">sym</property>
- <property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image235">
+ <property name="visible">True</property>
+ <property name="stock">gtk-goto-top</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</child>
- </widget>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkToolItem" id="toolitem16">
- <property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
<child>
- <widget class="GtkButton" id="transitivityButton">
- <property name="width_request">50</property>
+ <widget class="GtkButton" id="ScriptWinBackButton">
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">Transitivity</property>
+ <property name="tooltip" translatable="yes">go back 1 phrase</property>
<property name="can_focus">True</property>
- <property name="label" translatable="yes">trans</property>
- <property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image237">
+ <property name="visible">True</property>
+ <property name="stock">gtk-go-up</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</child>
- </widget>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkToolbar" id="toolbar8">
- <property name="visible">True</property>
- <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
- <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
- <property name="tooltips">True</property>
- <property name="show_arrow">True</property>
-
- <child>
- <widget class="GtkToolItem" id="toolitem22">
- <property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
<child>
- <widget class="GtkButton" id="simplifyButton">
- <property name="width_request">50</property>
+ <widget class="GtkButton" id="ScriptWinJumpButton">
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">Simplify</property>
+ <property name="tooltip" translatable="yes">execute until point</property>
<property name="can_focus">True</property>
- <property name="label" translatable="yes">simpl</property>
- <property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image134">
+ <property name="visible">True</property>
+ <property name="stock">gtk-jump-to</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</child>
- </widget>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkToolItem" id="toolitem23">
- <property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
<child>
- <widget class="GtkButton" id="reduceButton">
- <property name="width_request">50</property>
+ <widget class="GtkButton" id="ScriptWinForwardButton">
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">Reduce</property>
+ <property name="tooltip" translatable="yes">go forward 1 phrase</property>
<property name="can_focus">True</property>
- <property name="label" translatable="yes">red</property>
- <property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image239">
+ <property name="visible">True</property>
+ <property name="stock">gtk-go-down</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</child>
- </widget>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkToolItem" id="toolitem24">
- <property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
<child>
- <widget class="GtkButton" id="whdButton">
- <property name="width_request">50</property>
+ <widget class="GtkButton" id="ScriptWinBottomButton">
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">Whd</property>
+ <property name="tooltip" translatable="yes">execute all</property>
<property name="can_focus">True</property>
- <property name="label" translatable="yes">whd</property>
- <property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image238">
+ <property name="visible">True</property>
+ <property name="stock">gtk-goto-bottom</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</child>
</widget>
- <packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
</child>
</widget>
<packing>
<property name="padding">0</property>
<property name="expand">False</property>
- <property name="fill">False</property>
+ <property name="fill">True</property>
</packing>
</child>
<child>
- <widget class="GtkToolbar" id="toolbar6">
+ <widget class="GtkNotebook" id="ScriptNotebook">
<property name="visible">True</property>
- <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
- <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
- <property name="tooltips">True</property>
- <property name="show_arrow">True</property>
+ <property name="can_focus">True</property>
+ <property name="show_tabs">True</property>
+ <property name="show_border">True</property>
+ <property name="tab_pos">GTK_POS_BOTTOM</property>
+ <property name="scrollable">False</property>
+ <property name="enable_popup">False</property>
<child>
- <widget class="GtkToolItem" id="toolitem17">
+ <widget class="GtkScrolledWindow" id="ScrolledScript">
<property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_NONE</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
- <widget class="GtkButton" id="assumptionButton">
- <property name="width_request">50</property>
+ <widget class="GtkTextView" id="ScriptTextView">
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">Assumption</property>
<property name="can_focus">True</property>
- <property name="label" translatable="yes">asum</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
+ <property name="editable">True</property>
+ <property name="overwrite">False</property>
+ <property name="accepts_tab">True</property>
+ <property name="justification">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap_mode">GTK_WRAP_NONE</property>
+ <property name="cursor_visible">True</property>
+ <property name="pixels_above_lines">0</property>
+ <property name="pixels_below_lines">0</property>
+ <property name="pixels_inside_wrap">0</property>
+ <property name="left_margin">0</property>
+ <property name="right_margin">0</property>
+ <property name="indent">0</property>
+ <property name="text" translatable="yes"></property>
</widget>
</child>
</widget>
<packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkToolItem" id="toolitem18">
- <property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
-
- <child>
- <widget class="GtkButton" id="autoButton">
- <property name="width_request">50</property>
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Auto</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">auto</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- </widget>
- </child>
+ <property name="tab_expand">False</property>
+ <property name="tab_fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label7">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">script</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
</widget>
<packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
+ <property name="type">tab</property>
</packing>
</child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkToolbar" id="toolbar7">
- <property name="visible">True</property>
- <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
- <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
- <property name="tooltips">True</property>
- <property name="show_arrow">True</property>
<child>
- <widget class="GtkToolItem" id="toolitem20">
+ <widget class="GtkScrolledWindow" id="ScrolledOutline">
<property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
- <widget class="GtkButton" id="cutButton">
- <property name="width_request">50</property>
+ <widget class="GtkTreeView" id="OutlineTreeView">
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">Cut</property>
<property name="can_focus">True</property>
- <property name="label" translatable="yes">cut</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
+ <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="expand">False</property>
- <property name="homogeneous">False</property>
+ <property name="tab_expand">False</property>
+ <property name="tab_fill">True</property>
</packing>
</child>
<child>
- <widget class="GtkToolItem" id="toolitem21">
+ <widget class="GtkLabel" id="label8">
<property name="visible">True</property>
- <property name="visible_horizontal">True</property>
- <property name="visible_vertical">True</property>
- <property name="is_important">False</property>
-
- <child>
- <widget class="GtkButton" id="replaceButton">
- <property name="width_request">50</property>
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Replace</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">repl</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- </widget>
- </child>
+ <property name="label" translatable="yes">outline</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
</widget>
<packing>
- <property name="expand">False</property>
- <property name="homogeneous">False</property>
+ <property name="type">tab</property>
</packing>
</child>
</widget>
<packing>
<property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
</packing>
</child>
</widget>
</child>
</widget>
-<widget class="GtkDialog" id="ConfirmationDialog">
+<widget class="GtkDialog" id="TextDialog">
<property name="title" translatable="yes">DUMMY</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
- <property name="window_position">GTK_WIN_POS_CENTER</property>
- <property name="modal">True</property>
- <property name="resizable">False</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="resizable">True</property>
<property name="destroy_with_parent">False</property>
<property name="decorated">True</property>
<property name="skip_taskbar_hint">False</property>
<property name="has_separator">True</property>
<child internal-child="vbox">
- <widget class="GtkVBox" id="dialog-vbox1">
+ <widget class="GtkVBox" id="vbox5">
<property name="visible">True</property>
<property name="homogeneous">False</property>
<property name="spacing">0</property>
<child internal-child="action_area">
- <widget class="GtkHButtonBox" id="dialog-action_area1">
+ <widget class="GtkHButtonBox" id="hbuttonbox1">
<property name="visible">True</property>
<property name="layout_style">GTK_BUTTONBOX_END</property>
<child>
- <widget class="GtkButton" id="ConfirmationDialogCancelButton">
+ <widget class="GtkButton" id="TextDialogCancelButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
</child>
<child>
- <widget class="GtkButton" id="ConfirmationDialogOkButton">
+ <widget class="GtkButton" id="TextDialogOkButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
</child>
<child>
- <widget class="GtkLabel" id="ConfirmationDialogLabel">
+ <widget class="GtkLabel" id="TextDialogLabel">
<property name="visible">True</property>
<property name="label" translatable="yes">DUMMY</property>
<property name="use_underline">False</property>
<property name="use_markup">False</property>
- <property name="justify">GTK_JUSTIFY_CENTER</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="fill">False</property>
</packing>
</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="decorated">True</property>
- <property name="skip_taskbar_hint">False</property>
- <property name="skip_pager_hint">False</property>
- <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
- <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
- <property name="has_separator">True</property>
-
- <child internal-child="vbox">
- <widget class="GtkVBox" id="dialog-vbox2">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
- <child internal-child="action_area">
- <widget class="GtkHButtonBox" id="dialog-action_area2">
+ <child>
+ <widget class="GtkScrolledWindow" id="scrolledwindow2">
<property name="visible">True</property>
- <property name="layout_style">GTK_BUTTONBOX_END</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
- <widget class="GtkButton" id="AboutDismissButton">
+ <widget class="GtkTextView" id="TextDialogTextView">
<property name="visible">True</property>
- <property name="can_default">True</property>
<property name="can_focus">True</property>
- <property name="label">gtk-ok</property>
- <property name="use_stock">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- <property name="response_id">-5</property>
+ <property name="editable">True</property>
+ <property name="overwrite">False</property>
+ <property name="accepts_tab">True</property>
+ <property name="justification">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap_mode">GTK_WRAP_NONE</property>
+ <property name="cursor_visible">True</property>
+ <property name="pixels_above_lines">0</property>
+ <property name="pixels_below_lines">0</property>
+ <property name="pixels_inside_wrap">0</property>
+ <property name="left_margin">0</property>
+ <property name="right_margin">0</property>
+ <property name="indent">0</property>
+ <property name="text" translatable="yes"></property>
</widget>
</child>
</widget>
<packing>
<property name="padding">0</property>
- <property name="expand">False</property>
+ <property name="expand">True</property>
<property name="fill">True</property>
- <property name="pack_type">GTK_PACK_END</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkLabel" id="AboutLabel">
- <property name="visible">True</property>
- <property name="label" translatable="yes"><b>Matita @VERSION@</b>
-
-<tt>http://helm.cs.unibo.it</tt>
-
-Copyright (C) 2004,
-<i>the HELM team</i></property>
- <property name="use_underline">False</property>
- <property name="use_markup">True</property>
- <property name="justify">GTK_JUSTIFY_CENTER</property>
- <property name="wrap">False</property>
- <property name="selectable">False</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">5</property>
- <property name="ypad">5</property>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
</packing>
</child>
</widget>
</child>
</widget>
-<widget class="GtkDialog" id="UriChoiceDialog">
- <property name="height_request">280</property>
- <property name="title" translatable="yes">Uri choice</property>
+<widget class="GtkWindow" id="ToolBarWin">
+ <property name="width_request">155</property>
+ <property name="height_request">450</property>
+ <property name="title" translatable="yes">Tactics</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="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="resizable">False</property>
<property name="destroy_with_parent">False</property>
<property name="decorated">True</property>
<property name="skip_taskbar_hint">False</property>
<property name="skip_pager_hint">False</property>
- <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_TOOLBAR</property>
<property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
- <property name="has_separator">True</property>
- <child internal-child="vbox">
- <widget class="GtkVBox" id="dialog-vbox3">
+ <child>
+ <widget class="GtkEventBox" id="ToolBarEventBox">
<property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
+ <property name="visible_window">True</property>
+ <property name="above_child">False</property>
- <child internal-child="action_area">
- <widget class="GtkHButtonBox" id="dialog-action_area3">
+ <child>
+ <widget class="GtkVBox" id="ToolBarVBox">
<property name="visible">True</property>
- <property name="layout_style">GTK_BUTTONBOX_END</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
<child>
- <widget class="GtkButton" id="UriChoiceAbortButton">
+ <widget class="GtkToolbar" id="toolbar2">
<property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="label">gtk-cancel</property>
- <property name="use_stock">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- <property name="response_id">-6</property>
- </widget>
- </child>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
- <child>
- <widget class="GtkButton" id="UriChoiceSelectedButton">
- <property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- <property name="response_id">0</property>
+ <child>
+ <widget class="GtkToolItem" id="toolitem4">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="introsButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Intros</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">intros</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
<child>
- <widget class="GtkAlignment" id="alignment2">
+ <widget class="GtkToolItem" id="toolitem5">
<property name="visible">True</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xscale">0</property>
- <property name="yscale">0</property>
- <property name="top_padding">0</property>
- <property name="bottom_padding">0</property>
- <property name="left_padding">0</property>
- <property name="right_padding">0</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
<child>
- <widget class="GtkHBox" id="hbox3">
+ <widget class="GtkButton" id="applyButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">2</property>
+ <property name="tooltip" translatable="yes">Apply</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">apply</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
- <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="GtkToolItem" id="toolitem6">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
- <child>
- <widget class="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>
+ <child>
+ <widget class="GtkButton" id="exactButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Exact</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">exact</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
</widget>
</child>
</widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
</child>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</child>
<child>
- <widget class="GtkButton" id="UriChoiceConstantsButton">
- <property name="visible">True</property>
- <property name="sensitive">False</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="label" translatable="yes">Try Constants</property>
- <property name="use_underline">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- <property name="response_id">0</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkButton" id="UriChoiceAutoButton">
+ <widget class="GtkToolbar" id="toolbar3">
<property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- <property name="response_id">0</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
<child>
- <widget class="GtkAlignment" id="alignment1">
+ <widget class="GtkToolItem" id="toolitem7">
<property name="visible">True</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xscale">0</property>
- <property name="yscale">0</property>
- <property name="top_padding">0</property>
- <property name="bottom_padding">0</property>
- <property name="left_padding">0</property>
- <property name="right_padding">0</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
<child>
- <widget class="GtkHBox" id="hbox1">
+ <widget class="GtkButton" id="elimButton">
+ <property name="width_request">50</property>
<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>
+ <property name="tooltip" translatable="yes">Elim</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">elim</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
</widget>
</child>
</widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
</child>
- </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="GtkToolItem" id="toolitem8">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
- <child>
- <widget class="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>
+ <child>
+ <widget class="GtkButton" id="elimTypeButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">ElimType</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">elimTy</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
</widget>
<packing>
<property name="padding">0</property>
</child>
<child>
- <widget class="GtkScrolledWindow" id="scrolledwindow1">
+ <widget class="GtkToolbar" id="toolbar4">
<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>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
<child>
- <widget class="GtkTreeView" id="UriChoiceTreeView">
+ <widget class="GtkToolItem" id="toolitem9">
<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>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="splitButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Split</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">split</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
</widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
</child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">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">
+ <widget class="GtkToolItem" id="toolitem10">
<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>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="leftButton">
+ <property name="width_request">25</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Left</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">L</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
</widget>
<packing>
- <property name="padding">0</property>
<property name="expand">False</property>
- <property name="fill">False</property>
+ <property name="homogeneous">False</property>
</packing>
</child>
<child>
- <widget class="GtkEntry" id="entry1">
+ <widget class="GtkToolItem" id="toolitem11">
<property name="visible">True</property>
- <property name="can_focus">True</property>
- <property name="editable">True</property>
- <property name="visibility">True</property>
- <property name="max_length">0</property>
- <property name="text" translatable="yes"></property>
- <property name="has_frame">True</property>
- <property name="invisible_char">*</property>
- <property name="activates_default">False</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="rightButton">
+ <property name="width_request">25</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Right</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">R</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
</widget>
<packing>
- <property name="padding">0</property>
- <property name="expand">True</property>
- <property name="fill">True</property>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
</packing>
</child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">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="height_request">200</property>
- <property name="title" translatable="yes">Interpretation choice</property>
- <property name="type">GTK_WINDOW_TOPLEVEL</property>
- <property name="window_position">GTK_WIN_POS_NONE</property>
- <property name="modal">True</property>
- <property name="resizable">True</property>
- <property name="destroy_with_parent">False</property>
- <property name="decorated">True</property>
- <property name="skip_taskbar_hint">False</property>
- <property name="skip_pager_hint">False</property>
- <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
- <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
- <property name="has_separator">True</property>
-
- <child internal-child="vbox">
- <widget class="GtkVBox" id="dialog-vbox4">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
-
- <child internal-child="action_area">
- <widget class="GtkHButtonBox" id="dialog-action_area4">
- <property name="visible">True</property>
- <property name="layout_style">GTK_BUTTONBOX_END</property>
-
- <child>
- <widget class="GtkButton" id="InterpChoiceHelpButton">
- <property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="label">gtk-help</property>
- <property name="use_stock">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- <property name="response_id">-11</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkButton" id="InterpChoiceCancelButton">
- <property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="label">gtk-cancel</property>
- <property name="use_stock">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- <property name="response_id">-6</property>
- </widget>
- </child>
-
- <child>
- <widget class="GtkButton" id="InterpChoiceOkButton">
- <property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="label">gtk-ok</property>
- <property name="use_stock">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- <property name="response_id">-5</property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">True</property>
- <property name="pack_type">GTK_PACK_END</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkVBox" id="vbox3">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
-
- <child>
- <widget class="GtkLabel" id="InterpChoiceDialogLabel">
- <property name="visible">True</property>
- <property name="label" translatable="yes">some informative message here ...</property>
- <property name="use_underline">False</property>
- <property name="use_markup">False</property>
- <property name="justify">GTK_JUSTIFY_LEFT</property>
- <property name="wrap">False</property>
- <property name="selectable">False</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkScrolledWindow" id="scrolledwindow4">
- <property name="visible">True</property>
- <property name="can_focus">True</property>
- <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
- <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
- <property name="shadow_type">GTK_SHADOW_IN</property>
- <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
- <widget class="GtkTreeView" id="InterpChoiceTreeView">
+ <widget class="GtkToolItem" id="toolitem12">
<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>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="existsButton">
+ <property name="width_request">25</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Exists</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">∃</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
</widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
</child>
</widget>
<packing>
<property name="padding">0</property>
- <property name="expand">True</property>
- <property name="fill">True</property>
+ <property name="expand">False</property>
+ <property name="fill">False</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="EmptyDialog">
- <property name="visible">True</property>
- <property name="title" translatable="yes">DUMMY</property>
- <property name="type">GTK_WINDOW_TOPLEVEL</property>
- <property name="window_position">GTK_WIN_POS_NONE</property>
- <property name="modal">False</property>
- <property name="resizable">True</property>
- <property name="destroy_with_parent">False</property>
- <property name="decorated">True</property>
- <property name="skip_taskbar_hint">False</property>
- <property name="skip_pager_hint">False</property>
- <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
- <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
- <property name="has_separator">True</property>
-
- <child internal-child="vbox">
- <widget class="GtkVBox" id="EmptyDialogVBox">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
-
- <child internal-child="action_area">
- <widget class="GtkHButtonBox" id="dialog-action_area5">
- <property name="visible">True</property>
- <property name="layout_style">GTK_BUTTONBOX_END</property>
-
- <child>
- <widget class="GtkButton" id="EmptyDialogCancelButton">
- <property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="label">gtk-cancel</property>
- <property name="use_stock">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- <property name="response_id">-6</property>
- </widget>
- </child>
<child>
- <widget class="GtkButton" id="EmptyDialogOkButton">
+ <widget class="GtkToolbar" id="toolbar5">
<property name="visible">True</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="label">gtk-ok</property>
- <property name="use_stock">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
- <property name="response_id">-5</property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">True</property>
- <property name="pack_type">GTK_PACK_END</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkLabel" id="EmptyDialogLabel">
- <property name="visible">True</property>
- <property name="label" translatable="yes">DUMMY</property>
- <property name="use_underline">False</property>
- <property name="use_markup">False</property>
- <property name="justify">GTK_JUSTIFY_LEFT</property>
- <property name="wrap">False</property>
- <property name="selectable">False</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
-
- <child>
- <placeholder/>
- </child>
- </widget>
- </child>
-</widget>
-
-<widget class="GtkWindow" id="ScriptWin">
- <property name="title" translatable="yes">Matita: script</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">450</property>
- <property name="default_height">800</property>
- <property name="resizable">True</property>
- <property name="destroy_with_parent">False</property>
- <property name="decorated">True</property>
- <property name="skip_taskbar_hint">False</property>
- <property name="skip_pager_hint">False</property>
- <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
- <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
-
- <child>
- <widget class="GtkEventBox" id="ScriptWinEventBox">
- <property name="visible">True</property>
- <property name="visible_window">True</property>
- <property name="above_child">False</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
- <child>
- <widget class="GtkVBox" id="vbox7">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
+ <child>
+ <widget class="GtkToolItem" id="toolitem14">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
- <child>
- <widget class="GtkHandleBox" id="handlebox2">
- <property name="visible">True</property>
- <property name="shadow_type">GTK_SHADOW_OUT</property>
- <property name="handle_position">GTK_POS_LEFT</property>
- <property name="snap_edge">GTK_POS_TOP</property>
+ <child>
+ <widget class="GtkButton" id="reflexivityButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Reflexivity</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">refl</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
<child>
- <widget class="GtkHBox" id="hbox8">
+ <widget class="GtkToolItem" id="toolitem15">
<property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
<child>
- <widget class="GtkButton" id="ScriptWinTopButton">
+ <widget class="GtkButton" id="symmetryButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">restart</property>
+ <property name="tooltip" translatable="yes">Symmetry</property>
<property name="can_focus">True</property>
+ <property name="label" translatable="yes">sym</property>
+ <property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
-
- <child>
- <widget class="GtkImage" id="image235">
- <property name="visible">True</property>
- <property name="stock">gtk-goto-top</property>
- <property name="icon_size">4</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- </child>
</widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
</child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem16">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
<child>
- <widget class="GtkButton" id="ScriptWinBackButton">
+ <widget class="GtkButton" id="transitivityButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">go back 1 phrase</property>
+ <property name="tooltip" translatable="yes">Transitivity</property>
<property name="can_focus">True</property>
+ <property name="label" translatable="yes">trans</property>
+ <property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
-
- <child>
- <widget class="GtkImage" id="image133">
- <property name="visible">True</property>
- <property name="stock">gtk-undo</property>
- <property name="icon_size">4</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- </child>
</widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
</child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar8">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem22">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
<child>
- <widget class="GtkButton" id="ScriptWinJumpButton">
+ <widget class="GtkButton" id="simplifyButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">execute until point</property>
+ <property name="tooltip" translatable="yes">Simplify</property>
<property name="can_focus">True</property>
+ <property name="label" translatable="yes">simpl</property>
+ <property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
-
- <child>
- <widget class="GtkImage" id="image134">
- <property name="visible">True</property>
- <property name="stock">gtk-jump-to</property>
- <property name="icon_size">4</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- </child>
</widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
</child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem23">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
<child>
- <widget class="GtkButton" id="ScriptWinForwardButton">
+ <widget class="GtkButton" id="reduceButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">go forward 1 phrase</property>
+ <property name="tooltip" translatable="yes">Reduce</property>
<property name="can_focus">True</property>
+ <property name="label" translatable="yes">red</property>
+ <property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
-
- <child>
- <widget class="GtkImage" id="image135">
- <property name="visible">True</property>
- <property name="stock">gtk-redo</property>
- <property name="icon_size">4</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- </child>
</widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
</child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem24">
+ <property name="visible">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
<child>
- <widget class="GtkButton" id="ScriptWinBottomButton">
+ <widget class="GtkButton" id="whdButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">execute all</property>
+ <property name="tooltip" translatable="yes">Whd</property>
<property name="can_focus">True</property>
+ <property name="label" translatable="yes">whd</property>
+ <property name="use_underline">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
-
- <child>
- <widget class="GtkImage" id="image236">
- <property name="visible">True</property>
- <property name="stock">gtk-goto-bottom</property>
- <property name="icon_size">4</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- </child>
</widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
</child>
</widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
</child>
</widget>
<packing>
<property name="padding">0</property>
<property name="expand">False</property>
- <property name="fill">True</property>
+ <property name="fill">False</property>
</packing>
</child>
<child>
- <widget class="GtkNotebook" id="ScriptNotebook">
+ <widget class="GtkToolbar" id="toolbar6">
<property name="visible">True</property>
- <property name="can_focus">True</property>
- <property name="show_tabs">True</property>
- <property name="show_border">True</property>
- <property name="tab_pos">GTK_POS_BOTTOM</property>
- <property name="scrollable">False</property>
- <property name="enable_popup">False</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
<child>
- <widget class="GtkScrolledWindow" id="ScrolledScript">
+ <widget class="GtkToolItem" id="toolitem17">
<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>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
<child>
- <widget class="GtkTextView" id="ScriptTextView">
+ <widget class="GtkButton" id="assumptionButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Assumption</property>
<property name="can_focus">True</property>
- <property name="editable">True</property>
- <property name="overwrite">False</property>
- <property name="accepts_tab">True</property>
- <property name="justification">GTK_JUSTIFY_LEFT</property>
- <property name="wrap_mode">GTK_WRAP_NONE</property>
- <property name="cursor_visible">True</property>
- <property name="pixels_above_lines">0</property>
- <property name="pixels_below_lines">0</property>
- <property name="pixels_inside_wrap">0</property>
- <property name="left_margin">0</property>
- <property name="right_margin">0</property>
- <property name="indent">0</property>
- <property name="text" translatable="yes"></property>
+ <property name="label" translatable="yes">asum</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
</widget>
</child>
</widget>
<packing>
- <property name="tab_expand">False</property>
- <property name="tab_fill">True</property>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
</packing>
</child>
<child>
- <widget class="GtkLabel" id="label7">
+ <widget class="GtkToolItem" id="toolitem18">
<property name="visible">True</property>
- <property name="label" translatable="yes">script</property>
- <property name="use_underline">False</property>
- <property name="use_markup">False</property>
- <property name="justify">GTK_JUSTIFY_LEFT</property>
- <property name="wrap">False</property>
- <property name="selectable">False</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="autoButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Auto</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">auto</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
</widget>
<packing>
- <property name="type">tab</property>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
</packing>
</child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar7">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
<child>
- <widget class="GtkScrolledWindow" id="ScrolledOutline">
+ <widget class="GtkToolItem" id="toolitem20">
<property name="visible">True</property>
- <property name="can_focus">True</property>
- <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
- <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
- <property name="shadow_type">GTK_SHADOW_IN</property>
- <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
<child>
- <widget class="GtkTreeView" id="treeview1">
+ <widget class="GtkButton" id="cutButton">
+ <property name="width_request">50</property>
<property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Cut</property>
<property name="can_focus">True</property>
- <property name="headers_visible">False</property>
- <property name="rules_hint">False</property>
- <property name="reorderable">False</property>
- <property name="enable_search">True</property>
+ <property name="label" translatable="yes">cut</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
</widget>
</child>
</widget>
<packing>
- <property name="tab_expand">False</property>
- <property name="tab_fill">True</property>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
</packing>
</child>
<child>
- <widget class="GtkLabel" id="label8">
+ <widget class="GtkToolItem" id="toolitem21">
<property name="visible">True</property>
- <property name="label" translatable="yes">outline</property>
- <property name="use_underline">False</property>
- <property name="use_markup">False</property>
- <property name="justify">GTK_JUSTIFY_LEFT</property>
- <property name="wrap">False</property>
- <property name="selectable">False</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
+
+ <child>
+ <widget class="GtkButton" id="replaceButton">
+ <property name="width_request">50</property>
+ <property name="visible">True</property>
+ <property name="tooltip" translatable="yes">Replace</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">repl</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
</widget>
<packing>
- <property name="type">tab</property>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
</packing>
</child>
</widget>
<packing>
<property name="padding">0</property>
- <property name="expand">True</property>
- <property name="fill">True</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
</packing>
</child>
</widget>
</child>
</widget>
-<widget class="GtkDialog" id="TextDialog">
- <property name="title" translatable="yes">DUMMY</property>
+<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_NONE</property>
- <property name="modal">False</property>
+ <property name="window_position">GTK_WIN_POS_CENTER</property>
+ <property name="modal">True</property>
<property name="resizable">True</property>
<property name="destroy_with_parent">False</property>
<property name="decorated">True</property>
<property name="has_separator">True</property>
<child internal-child="vbox">
- <widget class="GtkVBox" id="vbox5">
+ <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="hbuttonbox1">
+ <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="TextDialogCancelButton">
+ <widget class="GtkButton" id="UriChoiceAbortButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
</child>
<child>
- <widget class="GtkButton" id="TextDialogOkButton">
+ <widget class="GtkButton" id="UriChoiceSelectedButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
- <property name="label">gtk-ok</property>
- <property name="use_stock">True</property>
<property name="relief">GTK_RELIEF_NORMAL</property>
<property name="focus_on_click">True</property>
- <property name="response_id">-5</property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">True</property>
- <property name="pack_type">GTK_PACK_END</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkLabel" id="TextDialogLabel">
- <property name="visible">True</property>
- <property name="label" translatable="yes">DUMMY</property>
- <property name="use_underline">False</property>
- <property name="use_markup">False</property>
- <property name="justify">GTK_JUSTIFY_LEFT</property>
- <property name="wrap">False</property>
- <property name="selectable">False</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkScrolledWindow" id="scrolledwindow2">
- <property name="visible">True</property>
- <property name="can_focus">True</property>
- <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
- <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
- <property name="shadow_type">GTK_SHADOW_IN</property>
- <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
-
- <child>
- <widget class="GtkTextView" id="TextDialogTextView">
- <property name="visible">True</property>
- <property name="can_focus">True</property>
- <property name="editable">True</property>
- <property name="overwrite">False</property>
- <property name="accepts_tab">True</property>
- <property name="justification">GTK_JUSTIFY_LEFT</property>
- <property name="wrap_mode">GTK_WRAP_NONE</property>
- <property name="cursor_visible">True</property>
- <property name="pixels_above_lines">0</property>
- <property name="pixels_below_lines">0</property>
- <property name="pixels_inside_wrap">0</property>
- <property name="left_margin">0</property>
- <property name="right_margin">0</property>
- <property name="indent">0</property>
- <property name="text" translatable="yes"></property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">True</property>
- <property name="fill">True</property>
- </packing>
- </child>
- </widget>
- </child>
-</widget>
-
-<widget class="GtkWindow" id="BrowserWin">
- <property name="width_request">400</property>
- <property name="height_request">500</property>
- <property name="visible">True</property>
- <property name="title" translatable="yes">Cic browser</property>
- <property name="type">GTK_WINDOW_TOPLEVEL</property>
- <property name="window_position">GTK_WIN_POS_NONE</property>
- <property name="modal">False</property>
- <property name="resizable">True</property>
- <property name="destroy_with_parent">False</property>
- <property name="decorated">True</property>
- <property name="skip_taskbar_hint">False</property>
- <property name="skip_pager_hint">False</property>
- <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
- <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
-
- <child>
- <widget class="GtkEventBox" id="BrowserWinEventBox">
- <property name="visible">True</property>
- <property name="visible_window">True</property>
- <property name="above_child">False</property>
-
- <child>
- <widget class="GtkVBox" id="BrowserVBox">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
-
- <child>
- <widget class="GtkHandleBox" id="handlebox1">
- <property name="visible">True</property>
- <property name="shadow_type">GTK_SHADOW_OUT</property>
- <property name="handle_position">GTK_POS_LEFT</property>
- <property name="snap_edge">GTK_POS_TOP</property>
+ <property name="response_id">0</property>
<child>
- <widget class="GtkHBox" id="hbox7">
+ <widget class="GtkAlignment" id="alignment2">
<property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xscale">0</property>
+ <property name="yscale">0</property>
+ <property name="top_padding">0</property>
+ <property name="bottom_padding">0</property>
+ <property name="left_padding">0</property>
+ <property name="right_padding">0</property>
<child>
- <widget class="GtkButton" id="BrowserNewButton">
+ <widget class="GtkHBox" id="hbox3">
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">new browser win</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
<child>
- <widget class="GtkImage" id="image191">
+ <widget class="GtkImage" id="image19">
<property name="visible">True</property>
- <property name="stock">gtk-new</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>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkButton" id="BrowserBackButton">
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">history back</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
-
- <child>
- <widget class="GtkAlignment" id="alignment3">
- <property name="visible">True</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xscale">0</property>
- <property name="yscale">0</property>
- <property name="top_padding">0</property>
- <property name="bottom_padding">0</property>
- <property name="left_padding">0</property>
- <property name="right_padding">0</property>
-
- <child>
- <widget class="GtkHBox" id="hbox6">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">2</property>
-
- <child>
- <widget class="GtkImage" id="image188">
- <property name="visible">True</property>
- <property name="stock">gtk-go-back</property>
- <property name="icon_size">4</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkLabel" id="label10">
- <property name="visible">True</property>
- <property name="label" translatable="yes"></property>
- <property name="use_underline">True</property>
- <property name="use_markup">False</property>
- <property name="justify">GTK_JUSTIFY_LEFT</property>
- <property name="wrap">False</property>
- <property name="selectable">False</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
- </widget>
- </child>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkButton" id="BrowserForwardButton">
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">history forward</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
<child>
- <widget class="GtkImage" id="image189">
+ <widget class="GtkLabel" id="label3">
<property name="visible">True</property>
- <property name="stock">gtk-go-forward</property>
- <property name="icon_size">4</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>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
</child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="UriChoiceConstantsButton">
+ <property name="visible">True</property>
+ <property name="sensitive">False</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">Try Constants</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">0</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="UriChoiceAutoButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ <property name="response_id">0</property>
+
+ <child>
+ <widget class="GtkAlignment" id="alignment1">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xscale">0</property>
+ <property name="yscale">0</property>
+ <property name="top_padding">0</property>
+ <property name="bottom_padding">0</property>
+ <property name="left_padding">0</property>
+ <property name="right_padding">0</property>
<child>
- <widget class="GtkButton" id="BrowserRefreshButton">
+ <widget class="GtkHBox" id="hbox1">
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">refresh</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
<child>
- <widget class="GtkImage" id="image229">
+ <widget class="GtkImage" id="image18">
<property name="visible">True</property>
- <property name="stock">gtk-refresh</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>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkButton" id="BrowserHomeButton">
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">home</property>
- <property name="can_default">True</property>
- <property name="can_focus">True</property>
- <property name="relief">GTK_RELIEF_NORMAL</property>
- <property name="focus_on_click">True</property>
<child>
- <widget class="GtkImage" id="image190">
+ <widget class="GtkLabel" id="label1">
<property name="visible">True</property>
- <property name="stock">gtk-home</property>
- <property name="icon_size">4</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>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">False</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkImage" id="image187">
- <property name="visible">True</property>
- <property name="stock">gtk-jump-to</property>
- <property name="icon_size">4</property>
- <property name="xalign">0.5</property>
- <property name="yalign">0.5</property>
- <property name="xpad">0</property>
- <property name="ypad">0</property>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">False</property>
- <property name="fill">True</property>
- </packing>
- </child>
-
- <child>
- <widget class="GtkEntry" id="BrowserUri">
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">cic uri</property>
- <property name="can_focus">True</property>
- <property name="editable">True</property>
- <property name="visibility">True</property>
- <property name="max_length">0</property>
- <property name="text" translatable="yes"></property>
- <property name="has_frame">True</property>
- <property name="invisible_char">*</property>
- <property name="activates_default">False</property>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">True</property>
- <property name="fill">True</property>
- </packing>
</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">True</property>
+ <property name="fill">False</property>
</packing>
</child>
<child>
- <widget class="GtkFrame" id="frame1">
+ <widget class="GtkScrolledWindow" id="scrolledwindow1">
<property name="visible">True</property>
- <property name="label_xalign">0</property>
- <property name="label_yalign">0</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="GtkScrolledWindow" id="ScrolledBrowser">
+ <widget class="GtkTreeView" id="UriChoiceTreeView">
<property name="visible">True</property>
<property name="can_focus">True</property>
- <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
- <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
- <property name="shadow_type">GTK_SHADOW_NONE</property>
- <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
-
- <child>
- <placeholder/>
- </child>
+ <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>
<property name="fill">True</property>
</packing>
</child>
+
+ <child>
+ <widget class="GtkHBox" id="hbox2">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkLabel" id="label2">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">URI: </property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkEntry" id="entry1">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="editable">True</property>
+ <property name="visibility">True</property>
+ <property name="max_length">0</property>
+ <property name="text" translatable="yes"></property>
+ <property name="has_frame">True</property>
+ <property name="invisible_char">*</property>
+ <property name="activates_default">False</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
</widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
</child>
</widget>
</child>
(* 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 mainWinEventBox =
- new GBin.event_box (GtkBin.EventBox.cast
- (Glade.get_widget_msg ~name:"MainWinEventBox" ~info:"GtkEventBox" xmldata))
- method mainWinEventBox = mainWinEventBox
- 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 image224 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image224" ~info:"GtkImage" xmldata))
- method image224 = image224
- 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 image225 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image225" ~info:"GtkImage" xmldata))
- method image225 = image225
- val saveMenuItem =
- new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
- (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
- method saveMenuItem = saveMenuItem
- val image226 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image226" ~info:"GtkImage" xmldata))
- method image226 = image226
- val saveAsMenuItem =
- new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
- (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
- method saveAsMenuItem = saveAsMenuItem
- val image227 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image227" ~info:"GtkImage" xmldata))
- method image227 = image227
- val separator1 =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" 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 image228 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image228" ~info:"GtkImage" xmldata))
- method image228 = image228
- 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 newCicBrowserMenuItem =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"NewCicBrowserMenuItem" ~info:"GtkMenuItem" xmldata))
- method newCicBrowserMenuItem = newCicBrowserMenuItem
- val showScriptMenuItem =
- new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
- (Glade.get_widget_msg ~name:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata))
- method showScriptMenuItem = showScriptMenuItem
- val separator3 =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"separator3" ~info:"GtkSeparatorMenuItem" xmldata))
- method separator3 = separator3
- val showConsoleMenuItem =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"ShowConsoleMenuItem" ~info:"GtkMenuItem" xmldata))
- method showConsoleMenuItem = showConsoleMenuItem
- 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 separator2 =
- new GMenu.menu_item (GtkMenu.MenuItem.cast
- (Glade.get_widget_msg ~name:"separator2" ~info:"GtkSeparatorMenuItem" xmldata))
- method separator2 = separator2
- 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 sequentsNotebook =
- new GPack.notebook (GtkPack.Notebook.cast
- (Glade.get_widget_msg ~name:"SequentsNotebook" ~info:"GtkNotebook" xmldata))
- method sequentsNotebook = sequentsNotebook
- val consoleEventBox =
- new GBin.event_box (GtkBin.EventBox.cast
- (Glade.get_widget_msg ~name:"ConsoleEventBox" ~info:"GtkEventBox" xmldata))
- method consoleEventBox = consoleEventBox
- val consoleHBox =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"ConsoleHBox" ~info:"GtkHBox" xmldata))
- method consoleHBox = consoleHBox
- val vbox6 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"vbox6" ~info:"GtkVBox" xmldata))
- method vbox6 = vbox6
- val hideConsoleButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"HideConsoleButton" ~info:"GtkButton" xmldata))
- method hideConsoleButton = hideConsoleButton
- val image169 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image169" ~info:"GtkImage" xmldata))
- method image169 = image169
- val scrolledConsole =
- new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
- (Glade.get_widget_msg ~name:"ScrolledConsole" ~info:"GtkScrolledWindow" xmldata))
- method scrolledConsole = scrolledConsole
- val mainStatusBar =
- new GMisc.statusbar (GtkMisc.Statusbar.cast
- (Glade.get_widget_msg ~name:"MainStatusBar" ~info:"GtkStatusbar" xmldata))
- method mainStatusBar = mainStatusBar
- method reparent parent =
- mainWinEventBox#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 fileSelCancelButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"fileSelCancelButton" ~info:"GtkButton" xmldata))
- method fileSelCancelButton = fileSelCancelButton
- val fileSelOkButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"fileSelOkButton" ~info:"GtkButton" xmldata))
- method fileSelOkButton = fileSelOkButton
- 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 toolBarVBox =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"ToolBarVBox" ~info:"GtkVBox" xmldata))
- method toolBarVBox = toolBarVBox
- val toolbar2 =
- new GButton.toolbar (GtkButton.Toolbar.cast
- (Glade.get_widget_msg ~name:"toolbar2" ~info:"GtkToolbar" xmldata))
- method toolbar2 = toolbar2
- val introsButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"introsButton" ~info:"GtkButton" xmldata))
- method introsButton = introsButton
- val applyButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"applyButton" ~info:"GtkButton" xmldata))
- method applyButton = applyButton
- val exactButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"exactButton" ~info:"GtkButton" xmldata))
- method exactButton = exactButton
- val toolbar3 =
- new GButton.toolbar (GtkButton.Toolbar.cast
- (Glade.get_widget_msg ~name:"toolbar3" ~info:"GtkToolbar" xmldata))
- method toolbar3 = toolbar3
- val elimButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"elimButton" ~info:"GtkButton" xmldata))
- method elimButton = elimButton
- val elimTypeButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"elimTypeButton" ~info:"GtkButton" xmldata))
- method elimTypeButton = elimTypeButton
- val toolbar4 =
- new GButton.toolbar (GtkButton.Toolbar.cast
- (Glade.get_widget_msg ~name:"toolbar4" ~info:"GtkToolbar" xmldata))
- method toolbar4 = toolbar4
- val splitButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"splitButton" ~info:"GtkButton" xmldata))
- method splitButton = splitButton
- val leftButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"leftButton" ~info:"GtkButton" xmldata))
- method leftButton = leftButton
- val rightButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"rightButton" ~info:"GtkButton" xmldata))
- method rightButton = rightButton
- val existsButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"existsButton" ~info:"GtkButton" xmldata))
- method existsButton = existsButton
- val toolbar5 =
- new GButton.toolbar (GtkButton.Toolbar.cast
- (Glade.get_widget_msg ~name:"toolbar5" ~info:"GtkToolbar" xmldata))
- method toolbar5 = toolbar5
- val reflexivityButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"reflexivityButton" ~info:"GtkButton" xmldata))
- method reflexivityButton = reflexivityButton
- val symmetryButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"symmetryButton" ~info:"GtkButton" xmldata))
- method symmetryButton = symmetryButton
- val transitivityButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"transitivityButton" ~info:"GtkButton" xmldata))
- method transitivityButton = transitivityButton
- val toolbar8 =
- new GButton.toolbar (GtkButton.Toolbar.cast
- (Glade.get_widget_msg ~name:"toolbar8" ~info:"GtkToolbar" xmldata))
- method toolbar8 = toolbar8
- val simplifyButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"simplifyButton" ~info:"GtkButton" xmldata))
- method simplifyButton = simplifyButton
- val reduceButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"reduceButton" ~info:"GtkButton" xmldata))
- method reduceButton = reduceButton
- val whdButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"whdButton" ~info:"GtkButton" xmldata))
- method whdButton = whdButton
- val toolbar6 =
- new GButton.toolbar (GtkButton.Toolbar.cast
- (Glade.get_widget_msg ~name:"toolbar6" ~info:"GtkToolbar" xmldata))
- method toolbar6 = toolbar6
- val assumptionButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"assumptionButton" ~info:"GtkButton" xmldata))
- method assumptionButton = assumptionButton
- val autoButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"autoButton" ~info:"GtkButton" xmldata))
- method autoButton = autoButton
- val toolbar7 =
- new GButton.toolbar (GtkButton.Toolbar.cast
- (Glade.get_widget_msg ~name:"toolbar7" ~info:"GtkToolbar" xmldata))
- method toolbar7 = toolbar7
- val cutButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"cutButton" ~info:"GtkButton" xmldata))
- method cutButton = cutButton
- val replaceButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"replaceButton" ~info:"GtkButton" xmldata))
- method replaceButton = replaceButton
- method reparent parent =
- toolBarEventBox#misc#reparent parent;
- toplevel#destroy ()
- method check_widgets () = ()
- end
-class confirmationDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"ConfirmationDialog" ?domain () in
- object (self)
- inherit Glade.xml ?autoconnect xmldata
- val toplevel =
- new GWindow.dialog_any (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata))
- method toplevel = toplevel
- val confirmationDialog =
- new GWindow.dialog_any (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata))
- method confirmationDialog = confirmationDialog
- 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 dialog_action_area1 =
- new GPack.button_box (GtkPack.BBox.cast
- (Glade.get_widget_msg ~name:"dialog-action_area1" ~info:"GtkHButtonBox" xmldata))
- method dialog_action_area1 = dialog_action_area1
- val confirmationDialogCancelButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"ConfirmationDialogCancelButton" ~info:"GtkButton" xmldata))
- method confirmationDialogCancelButton = confirmationDialogCancelButton
- val confirmationDialogOkButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"ConfirmationDialogOkButton" ~info:"GtkButton" xmldata))
- method confirmationDialogOkButton = confirmationDialogOkButton
- val confirmationDialogLabel =
- new GMisc.label (GtkMisc.Label.cast
- (Glade.get_widget_msg ~name:"ConfirmationDialogLabel" ~info:"GtkLabel" xmldata))
- method confirmationDialogLabel = confirmationDialogLabel
- 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)
toplevel#destroy ()
method check_widgets () = ()
end
-class uriChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"UriChoiceDialog" ?domain () in
+class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"BrowserWin" ?domain () in
object (self)
inherit Glade.xml ?autoconnect xmldata
val toplevel =
- new GWindow.dialog_any (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata))
+ new GWindow.window (GtkWindow.Window.cast
+ (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata))
method toplevel = toplevel
- val uriChoiceDialog =
- new GWindow.dialog_any (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata))
- method uriChoiceDialog = uriChoiceDialog
- val dialog_vbox3 =
+ val browserWin =
+ new GWindow.window (GtkWindow.Window.cast
+ (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata))
+ method browserWin = browserWin
+ val browserWinEventBox =
+ new GBin.event_box (GtkBin.EventBox.cast
+ (Glade.get_widget_msg ~name:"BrowserWinEventBox" ~info:"GtkEventBox" xmldata))
+ method browserWinEventBox = browserWinEventBox
+ val browserVBox =
new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"dialog-vbox3" ~info:"GtkVBox" xmldata))
- method dialog_vbox3 = dialog_vbox3
- val dialog_action_area3 =
- new GPack.button_box (GtkPack.BBox.cast
- (Glade.get_widget_msg ~name:"dialog-action_area3" ~info:"GtkHButtonBox" xmldata))
- method dialog_action_area3 = dialog_action_area3
- val uriChoiceAbortButton =
+ (Glade.get_widget_msg ~name:"BrowserVBox" ~info:"GtkVBox" xmldata))
+ method browserVBox = browserVBox
+ val handlebox1 =
+ new GBin.handle_box (GtkBin.HandleBox.cast
+ (Glade.get_widget_msg ~name:"handlebox1" ~info:"GtkHandleBox" xmldata))
+ method handlebox1 = handlebox1
+ val hbox7 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"hbox7" ~info:"GtkHBox" xmldata))
+ method hbox7 = hbox7
+ val browserNewButton =
new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"UriChoiceAbortButton" ~info:"GtkButton" xmldata))
- method uriChoiceAbortButton = uriChoiceAbortButton
- val uriChoiceSelectedButton =
+ (Glade.get_widget_msg ~name:"BrowserNewButton" ~info:"GtkButton" xmldata))
+ method browserNewButton = browserNewButton
+ val image191 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image191" ~info:"GtkImage" xmldata))
+ method image191 = image191
+ val browserBackButton =
new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"UriChoiceSelectedButton" ~info:"GtkButton" xmldata))
- method uriChoiceSelectedButton = uriChoiceSelectedButton
- val alignment2 =
+ (Glade.get_widget_msg ~name:"BrowserBackButton" ~info:"GtkButton" xmldata))
+ method browserBackButton = browserBackButton
+ val alignment3 =
new GBin.alignment (GtkBin.Alignment.cast
- (Glade.get_widget_msg ~name:"alignment2" ~info:"GtkAlignment" xmldata))
- method alignment2 = alignment2
- val hbox3 =
+ (Glade.get_widget_msg ~name:"alignment3" ~info:"GtkAlignment" xmldata))
+ method alignment3 = alignment3
+ val hbox6 =
new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"hbox3" ~info:"GtkHBox" xmldata))
- method hbox3 = hbox3
- val image19 =
+ (Glade.get_widget_msg ~name:"hbox6" ~info:"GtkHBox" xmldata))
+ method hbox6 = hbox6
+ val image188 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image19" ~info:"GtkImage" xmldata))
- method image19 = image19
- val label3 =
+ (Glade.get_widget_msg ~name:"image188" ~info:"GtkImage" xmldata))
+ method image188 = image188
+ val label10 =
new GMisc.label (GtkMisc.Label.cast
- (Glade.get_widget_msg ~name:"label3" ~info:"GtkLabel" xmldata))
- method label3 = label3
- val uriChoiceConstantsButton =
+ (Glade.get_widget_msg ~name:"label10" ~info:"GtkLabel" xmldata))
+ method label10 = label10
+ val browserForwardButton =
new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"UriChoiceConstantsButton" ~info:"GtkButton" xmldata))
- method uriChoiceConstantsButton = uriChoiceConstantsButton
- val uriChoiceAutoButton =
+ (Glade.get_widget_msg ~name:"BrowserForwardButton" ~info:"GtkButton" xmldata))
+ method browserForwardButton = browserForwardButton
+ val image189 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image189" ~info:"GtkImage" xmldata))
+ method image189 = image189
+ val browserRefreshButton =
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 =
+ (Glade.get_widget_msg ~name:"BrowserRefreshButton" ~info:"GtkButton" xmldata))
+ method browserRefreshButton = browserRefreshButton
+ val image229 =
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 =
+ (Glade.get_widget_msg ~name:"image229" ~info:"GtkImage" xmldata))
+ method image229 = image229
+ val browserHomeButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"BrowserHomeButton" ~info:"GtkButton" xmldata))
+ method browserHomeButton = browserHomeButton
+ val image190 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image190" ~info:"GtkImage" xmldata))
+ method image190 = image190
+ val image187 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image187" ~info:"GtkImage" xmldata))
+ method image187 = image187
+ val browserUri =
+ new GEdit.entry (GtkEdit.Entry.cast
+ (Glade.get_widget_msg ~name:"BrowserUri" ~info:"GtkEntry" xmldata))
+ method browserUri = browserUri
+ val frame1 =
+ new GBin.frame (GtkBin.Frame.cast
+ (Glade.get_widget_msg ~name:"frame1" ~info:"GtkFrame" xmldata))
+ method frame1 = frame1
+ val scrolledBrowser =
+ new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+ (Glade.get_widget_msg ~name:"ScrolledBrowser" ~info:"GtkScrolledWindow" xmldata))
+ method scrolledBrowser = scrolledBrowser
+ method reparent parent =
+ browserWinEventBox#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+class confirmationDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"ConfirmationDialog" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel =
+ new GWindow.dialog_any (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata))
+ method toplevel = toplevel
+ val confirmationDialog =
+ new GWindow.dialog_any (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata))
+ method confirmationDialog = confirmationDialog
+ val dialog_vbox1 =
new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"vbox2" ~info:"GtkVBox" xmldata))
- method vbox2 = vbox2
- val uriChoiceLabel =
+ (Glade.get_widget_msg ~name:"dialog-vbox1" ~info:"GtkVBox" xmldata))
+ method dialog_vbox1 = dialog_vbox1
+ val dialog_action_area1 =
+ new GPack.button_box (GtkPack.BBox.cast
+ (Glade.get_widget_msg ~name:"dialog-action_area1" ~info:"GtkHButtonBox" xmldata))
+ method dialog_action_area1 = dialog_action_area1
+ val confirmationDialogCancelButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"ConfirmationDialogCancelButton" ~info:"GtkButton" xmldata))
+ method confirmationDialogCancelButton = confirmationDialogCancelButton
+ val confirmationDialogOkButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"ConfirmationDialogOkButton" ~info:"GtkButton" xmldata))
+ method confirmationDialogOkButton = confirmationDialogOkButton
+ val confirmationDialogLabel =
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 =
+ (Glade.get_widget_msg ~name:"ConfirmationDialogLabel" ~info:"GtkLabel" xmldata))
+ method confirmationDialogLabel = confirmationDialogLabel
+ method reparent parent =
+ dialog_vbox1#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+class emptyDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"EmptyDialog" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel =
+ new GWindow.dialog_any (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata))
+ method toplevel = toplevel
+ val emptyDialog =
+ new GWindow.dialog_any (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata))
+ method emptyDialog = emptyDialog
+ val emptyDialogVBox =
new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"hbox2" ~info:"GtkHBox" xmldata))
- method hbox2 = hbox2
- val label2 =
+ (Glade.get_widget_msg ~name:"EmptyDialogVBox" ~info:"GtkVBox" xmldata))
+ method emptyDialogVBox = emptyDialogVBox
+ val dialog_action_area5 =
+ new GPack.button_box (GtkPack.BBox.cast
+ (Glade.get_widget_msg ~name:"dialog-action_area5" ~info:"GtkHButtonBox" xmldata))
+ method dialog_action_area5 = dialog_action_area5
+ val emptyDialogCancelButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"EmptyDialogCancelButton" ~info:"GtkButton" xmldata))
+ method emptyDialogCancelButton = emptyDialogCancelButton
+ val emptyDialogOkButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"EmptyDialogOkButton" ~info:"GtkButton" xmldata))
+ method emptyDialogOkButton = emptyDialogOkButton
+ val emptyDialogLabel =
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
+ (Glade.get_widget_msg ~name:"EmptyDialogLabel" ~info:"GtkLabel" xmldata))
+ method emptyDialogLabel = emptyDialogLabel
method reparent parent =
- dialog_vbox3#misc#reparent parent;
+ emptyDialogVBox#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 fileSelCancelButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"fileSelCancelButton" ~info:"GtkButton" xmldata))
+ method fileSelCancelButton = fileSelCancelButton
+ val fileSelOkButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"fileSelOkButton" ~info:"GtkButton" xmldata))
+ method fileSelOkButton = fileSelOkButton
+ method check_widgets () = ()
+ end
class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
let xmldata = Glade.create ~file ~root:"InterpChoiceDialog" ?domain () in
object (self)
method interpChoiceOkButton = interpChoiceOkButton
val vbox3 =
new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"vbox3" ~info:"GtkVBox" xmldata))
- method vbox3 = vbox3
- val interpChoiceDialogLabel =
- new GMisc.label (GtkMisc.Label.cast
- (Glade.get_widget_msg ~name:"InterpChoiceDialogLabel" ~info:"GtkLabel" xmldata))
- method interpChoiceDialogLabel = interpChoiceDialogLabel
- val scrolledwindow4 =
- new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
- (Glade.get_widget_msg ~name:"scrolledwindow4" ~info:"GtkScrolledWindow" xmldata))
- method scrolledwindow4 = scrolledwindow4
- val interpChoiceTreeView =
- new GTree.view (GtkTree.TreeView.cast
- (Glade.get_widget_msg ~name:"InterpChoiceTreeView" ~info:"GtkTreeView" xmldata))
- method interpChoiceTreeView = interpChoiceTreeView
- method reparent parent =
- dialog_vbox4#misc#reparent parent;
- toplevel#destroy ()
- method check_widgets () = ()
- end
-class emptyDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"EmptyDialog" ?domain () in
- object (self)
- inherit Glade.xml ?autoconnect xmldata
- val toplevel =
- new GWindow.dialog_any (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata))
- method toplevel = toplevel
- val emptyDialog =
- new GWindow.dialog_any (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata))
- method emptyDialog = emptyDialog
- val emptyDialogVBox =
+ (Glade.get_widget_msg ~name:"vbox3" ~info:"GtkVBox" xmldata))
+ method vbox3 = vbox3
+ val interpChoiceDialogLabel =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"InterpChoiceDialogLabel" ~info:"GtkLabel" xmldata))
+ method interpChoiceDialogLabel = interpChoiceDialogLabel
+ val scrolledwindow4 =
+ new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+ (Glade.get_widget_msg ~name:"scrolledwindow4" ~info:"GtkScrolledWindow" xmldata))
+ method scrolledwindow4 = scrolledwindow4
+ val interpChoiceTreeView =
+ new GTree.view (GtkTree.TreeView.cast
+ (Glade.get_widget_msg ~name:"InterpChoiceTreeView" ~info:"GtkTreeView" xmldata))
+ method interpChoiceTreeView = interpChoiceTreeView
+ method reparent parent =
+ dialog_vbox4#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+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 mainWinEventBox =
+ new GBin.event_box (GtkBin.EventBox.cast
+ (Glade.get_widget_msg ~name:"MainWinEventBox" ~info:"GtkEventBox" xmldata))
+ method mainWinEventBox = mainWinEventBox
+ 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 image224 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image224" ~info:"GtkImage" xmldata))
+ method image224 = image224
+ 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 image225 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image225" ~info:"GtkImage" xmldata))
+ method image225 = image225
+ val saveMenuItem =
+ new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+ (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
+ method saveMenuItem = saveMenuItem
+ val image226 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image226" ~info:"GtkImage" xmldata))
+ method image226 = image226
+ val saveAsMenuItem =
+ new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+ (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
+ method saveAsMenuItem = saveAsMenuItem
+ val image227 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image227" ~info:"GtkImage" xmldata))
+ method image227 = image227
+ val separator1 =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" 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 image228 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image228" ~info:"GtkImage" xmldata))
+ method image228 = image228
+ 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 newCicBrowserMenuItem =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"NewCicBrowserMenuItem" ~info:"GtkMenuItem" xmldata))
+ method newCicBrowserMenuItem = newCicBrowserMenuItem
+ val showScriptMenuItem =
+ new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
+ (Glade.get_widget_msg ~name:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata))
+ method showScriptMenuItem = showScriptMenuItem
+ val separator3 =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"separator3" ~info:"GtkSeparatorMenuItem" xmldata))
+ method separator3 = separator3
+ val showConsoleMenuItem =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"ShowConsoleMenuItem" ~info:"GtkMenuItem" xmldata))
+ method showConsoleMenuItem = showConsoleMenuItem
+ 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 separator2 =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"separator2" ~info:"GtkSeparatorMenuItem" xmldata))
+ method separator2 = separator2
+ 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 sequentsNotebook =
+ new GPack.notebook (GtkPack.Notebook.cast
+ (Glade.get_widget_msg ~name:"SequentsNotebook" ~info:"GtkNotebook" xmldata))
+ method sequentsNotebook = sequentsNotebook
+ val consoleEventBox =
+ new GBin.event_box (GtkBin.EventBox.cast
+ (Glade.get_widget_msg ~name:"ConsoleEventBox" ~info:"GtkEventBox" xmldata))
+ method consoleEventBox = consoleEventBox
+ val consoleHBox =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"ConsoleHBox" ~info:"GtkHBox" xmldata))
+ method consoleHBox = consoleHBox
+ val vbox6 =
new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"EmptyDialogVBox" ~info:"GtkVBox" xmldata))
- method emptyDialogVBox = emptyDialogVBox
- val dialog_action_area5 =
- new GPack.button_box (GtkPack.BBox.cast
- (Glade.get_widget_msg ~name:"dialog-action_area5" ~info:"GtkHButtonBox" xmldata))
- method dialog_action_area5 = dialog_action_area5
- val emptyDialogCancelButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"EmptyDialogCancelButton" ~info:"GtkButton" xmldata))
- method emptyDialogCancelButton = emptyDialogCancelButton
- val emptyDialogOkButton =
+ (Glade.get_widget_msg ~name:"vbox6" ~info:"GtkVBox" xmldata))
+ method vbox6 = vbox6
+ val hideConsoleButton =
new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"EmptyDialogOkButton" ~info:"GtkButton" xmldata))
- method emptyDialogOkButton = emptyDialogOkButton
- val emptyDialogLabel =
- new GMisc.label (GtkMisc.Label.cast
- (Glade.get_widget_msg ~name:"EmptyDialogLabel" ~info:"GtkLabel" xmldata))
- method emptyDialogLabel = emptyDialogLabel
+ (Glade.get_widget_msg ~name:"HideConsoleButton" ~info:"GtkButton" xmldata))
+ method hideConsoleButton = hideConsoleButton
+ val image169 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image169" ~info:"GtkImage" xmldata))
+ method image169 = image169
+ val scrolledConsole =
+ new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+ (Glade.get_widget_msg ~name:"ScrolledConsole" ~info:"GtkScrolledWindow" xmldata))
+ method scrolledConsole = scrolledConsole
+ val mainStatusBar =
+ new GMisc.statusbar (GtkMisc.Statusbar.cast
+ (Glade.get_widget_msg ~name:"MainStatusBar" ~info:"GtkStatusbar" xmldata))
+ method mainStatusBar = mainStatusBar
method reparent parent =
- emptyDialogVBox#misc#reparent parent;
+ mainWinEventBox#misc#reparent parent;
toplevel#destroy ()
method check_widgets () = ()
end
new GButton.button (GtkButton.Button.cast
(Glade.get_widget_msg ~name:"ScriptWinBackButton" ~info:"GtkButton" xmldata))
method scriptWinBackButton = scriptWinBackButton
- val image133 =
+ val image237 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image133" ~info:"GtkImage" xmldata))
- method image133 = image133
+ (Glade.get_widget_msg ~name:"image237" ~info:"GtkImage" xmldata))
+ method image237 = image237
val scriptWinJumpButton =
new GButton.button (GtkButton.Button.cast
(Glade.get_widget_msg ~name:"ScriptWinJumpButton" ~info:"GtkButton" xmldata))
new GButton.button (GtkButton.Button.cast
(Glade.get_widget_msg ~name:"ScriptWinForwardButton" ~info:"GtkButton" xmldata))
method scriptWinForwardButton = scriptWinForwardButton
- val image135 =
+ val image239 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image135" ~info:"GtkImage" xmldata))
- method image135 = image135
+ (Glade.get_widget_msg ~name:"image239" ~info:"GtkImage" xmldata))
+ method image239 = image239
val scriptWinBottomButton =
new GButton.button (GtkButton.Button.cast
(Glade.get_widget_msg ~name:"ScriptWinBottomButton" ~info:"GtkButton" xmldata))
method scriptWinBottomButton = scriptWinBottomButton
- val image236 =
+ val image238 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image236" ~info:"GtkImage" xmldata))
- method image236 = image236
+ (Glade.get_widget_msg ~name:"image238" ~info:"GtkImage" xmldata))
+ method image238 = image238
val scriptNotebook =
new GPack.notebook (GtkPack.Notebook.cast
(Glade.get_widget_msg ~name:"ScriptNotebook" ~info:"GtkNotebook" xmldata))
new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
(Glade.get_widget_msg ~name:"ScrolledOutline" ~info:"GtkScrolledWindow" xmldata))
method scrolledOutline = scrolledOutline
- val treeview1 =
+ val outlineTreeView =
new GTree.view (GtkTree.TreeView.cast
- (Glade.get_widget_msg ~name:"treeview1" ~info:"GtkTreeView" xmldata))
- method treeview1 = treeview1
+ (Glade.get_widget_msg ~name:"OutlineTreeView" ~info:"GtkTreeView" xmldata))
+ method outlineTreeView = outlineTreeView
val label8 =
new GMisc.label (GtkMisc.Label.cast
(Glade.get_widget_msg ~name:"label8" ~info:"GtkLabel" xmldata))
method label8 = label8
method reparent parent =
- scriptWinEventBox#misc#reparent parent;
+ scriptWinEventBox#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+class textDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"TextDialog" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel =
+ new GWindow.dialog_any (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata))
+ method toplevel = toplevel
+ val textDialog =
+ new GWindow.dialog_any (GtkWindow.Dialog.cast
+ (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata))
+ method textDialog = textDialog
+ val vbox5 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"vbox5" ~info:"GtkVBox" xmldata))
+ method vbox5 = vbox5
+ val hbuttonbox1 =
+ new GPack.button_box (GtkPack.BBox.cast
+ (Glade.get_widget_msg ~name:"hbuttonbox1" ~info:"GtkHButtonBox" xmldata))
+ method hbuttonbox1 = hbuttonbox1
+ val textDialogCancelButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"TextDialogCancelButton" ~info:"GtkButton" xmldata))
+ method textDialogCancelButton = textDialogCancelButton
+ val textDialogOkButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"TextDialogOkButton" ~info:"GtkButton" xmldata))
+ method textDialogOkButton = textDialogOkButton
+ val textDialogLabel =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"TextDialogLabel" ~info:"GtkLabel" xmldata))
+ method textDialogLabel = textDialogLabel
+ val scrolledwindow2 =
+ new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+ (Glade.get_widget_msg ~name:"scrolledwindow2" ~info:"GtkScrolledWindow" xmldata))
+ method scrolledwindow2 = scrolledwindow2
+ val textDialogTextView =
+ new GText.view (GtkText.View.cast
+ (Glade.get_widget_msg ~name:"TextDialogTextView" ~info:"GtkTextView" xmldata))
+ method textDialogTextView = textDialogTextView
+ method reparent parent =
+ vbox5#misc#reparent parent;
+ toplevel#destroy ()
+ 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 toolBarVBox =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"ToolBarVBox" ~info:"GtkVBox" xmldata))
+ method toolBarVBox = toolBarVBox
+ val toolbar2 =
+ new GButton.toolbar (GtkButton.Toolbar.cast
+ (Glade.get_widget_msg ~name:"toolbar2" ~info:"GtkToolbar" xmldata))
+ method toolbar2 = toolbar2
+ val introsButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"introsButton" ~info:"GtkButton" xmldata))
+ method introsButton = introsButton
+ val applyButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"applyButton" ~info:"GtkButton" xmldata))
+ method applyButton = applyButton
+ val exactButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"exactButton" ~info:"GtkButton" xmldata))
+ method exactButton = exactButton
+ val toolbar3 =
+ new GButton.toolbar (GtkButton.Toolbar.cast
+ (Glade.get_widget_msg ~name:"toolbar3" ~info:"GtkToolbar" xmldata))
+ method toolbar3 = toolbar3
+ val elimButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"elimButton" ~info:"GtkButton" xmldata))
+ method elimButton = elimButton
+ val elimTypeButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"elimTypeButton" ~info:"GtkButton" xmldata))
+ method elimTypeButton = elimTypeButton
+ val toolbar4 =
+ new GButton.toolbar (GtkButton.Toolbar.cast
+ (Glade.get_widget_msg ~name:"toolbar4" ~info:"GtkToolbar" xmldata))
+ method toolbar4 = toolbar4
+ val splitButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"splitButton" ~info:"GtkButton" xmldata))
+ method splitButton = splitButton
+ val leftButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"leftButton" ~info:"GtkButton" xmldata))
+ method leftButton = leftButton
+ val rightButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"rightButton" ~info:"GtkButton" xmldata))
+ method rightButton = rightButton
+ val existsButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"existsButton" ~info:"GtkButton" xmldata))
+ method existsButton = existsButton
+ val toolbar5 =
+ new GButton.toolbar (GtkButton.Toolbar.cast
+ (Glade.get_widget_msg ~name:"toolbar5" ~info:"GtkToolbar" xmldata))
+ method toolbar5 = toolbar5
+ val reflexivityButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"reflexivityButton" ~info:"GtkButton" xmldata))
+ method reflexivityButton = reflexivityButton
+ val symmetryButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"symmetryButton" ~info:"GtkButton" xmldata))
+ method symmetryButton = symmetryButton
+ val transitivityButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"transitivityButton" ~info:"GtkButton" xmldata))
+ method transitivityButton = transitivityButton
+ val toolbar8 =
+ new GButton.toolbar (GtkButton.Toolbar.cast
+ (Glade.get_widget_msg ~name:"toolbar8" ~info:"GtkToolbar" xmldata))
+ method toolbar8 = toolbar8
+ val simplifyButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"simplifyButton" ~info:"GtkButton" xmldata))
+ method simplifyButton = simplifyButton
+ val reduceButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"reduceButton" ~info:"GtkButton" xmldata))
+ method reduceButton = reduceButton
+ val whdButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"whdButton" ~info:"GtkButton" xmldata))
+ method whdButton = whdButton
+ val toolbar6 =
+ new GButton.toolbar (GtkButton.Toolbar.cast
+ (Glade.get_widget_msg ~name:"toolbar6" ~info:"GtkToolbar" xmldata))
+ method toolbar6 = toolbar6
+ val assumptionButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"assumptionButton" ~info:"GtkButton" xmldata))
+ method assumptionButton = assumptionButton
+ val autoButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"autoButton" ~info:"GtkButton" xmldata))
+ method autoButton = autoButton
+ val toolbar7 =
+ new GButton.toolbar (GtkButton.Toolbar.cast
+ (Glade.get_widget_msg ~name:"toolbar7" ~info:"GtkToolbar" xmldata))
+ method toolbar7 = toolbar7
+ val cutButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"cutButton" ~info:"GtkButton" xmldata))
+ method cutButton = cutButton
+ val replaceButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"replaceButton" ~info:"GtkButton" xmldata))
+ method replaceButton = replaceButton
+ method reparent parent =
+ toolBarEventBox#misc#reparent parent;
toplevel#destroy ()
method check_widgets () = ()
end
-class textDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"TextDialog" ?domain () in
+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 =
new GWindow.dialog_any (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata))
+ (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata))
method toplevel = toplevel
- val textDialog =
+ val uriChoiceDialog =
new GWindow.dialog_any (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata))
- method textDialog = textDialog
- val vbox5 =
+ (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:"vbox5" ~info:"GtkVBox" xmldata))
- method vbox5 = vbox5
- val hbuttonbox1 =
+ (Glade.get_widget_msg ~name:"dialog-vbox3" ~info:"GtkVBox" xmldata))
+ method dialog_vbox3 = dialog_vbox3
+ val dialog_action_area3 =
new GPack.button_box (GtkPack.BBox.cast
- (Glade.get_widget_msg ~name:"hbuttonbox1" ~info:"GtkHButtonBox" xmldata))
- method hbuttonbox1 = hbuttonbox1
- val textDialogCancelButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"TextDialogCancelButton" ~info:"GtkButton" xmldata))
- method textDialogCancelButton = textDialogCancelButton
- val textDialogOkButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"TextDialogOkButton" ~info:"GtkButton" xmldata))
- method textDialogOkButton = textDialogOkButton
- val textDialogLabel =
- new GMisc.label (GtkMisc.Label.cast
- (Glade.get_widget_msg ~name:"TextDialogLabel" ~info:"GtkLabel" xmldata))
- method textDialogLabel = textDialogLabel
- val scrolledwindow2 =
- new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
- (Glade.get_widget_msg ~name:"scrolledwindow2" ~info:"GtkScrolledWindow" xmldata))
- method scrolledwindow2 = scrolledwindow2
- val textDialogTextView =
- new GText.view (GtkText.View.cast
- (Glade.get_widget_msg ~name:"TextDialogTextView" ~info:"GtkTextView" xmldata))
- method textDialogTextView = textDialogTextView
- method reparent parent =
- vbox5#misc#reparent parent;
- toplevel#destroy ()
- method check_widgets () = ()
- end
-class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"BrowserWin" ?domain () in
- object (self)
- inherit Glade.xml ?autoconnect xmldata
- val toplevel =
- new GWindow.window (GtkWindow.Window.cast
- (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata))
- method toplevel = toplevel
- val browserWin =
- new GWindow.window (GtkWindow.Window.cast
- (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata))
- method browserWin = browserWin
- val browserWinEventBox =
- new GBin.event_box (GtkBin.EventBox.cast
- (Glade.get_widget_msg ~name:"BrowserWinEventBox" ~info:"GtkEventBox" xmldata))
- method browserWinEventBox = browserWinEventBox
- val browserVBox =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"BrowserVBox" ~info:"GtkVBox" xmldata))
- method browserVBox = browserVBox
- val handlebox1 =
- new GBin.handle_box (GtkBin.HandleBox.cast
- (Glade.get_widget_msg ~name:"handlebox1" ~info:"GtkHandleBox" xmldata))
- method handlebox1 = handlebox1
- val hbox7 =
- new GPack.box (GtkPack.Box.cast
- (Glade.get_widget_msg ~name:"hbox7" ~info:"GtkHBox" xmldata))
- method hbox7 = hbox7
- val browserNewButton =
+ (Glade.get_widget_msg ~name:"dialog-action_area3" ~info:"GtkHButtonBox" xmldata))
+ method dialog_action_area3 = dialog_action_area3
+ val uriChoiceAbortButton =
new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"BrowserNewButton" ~info:"GtkButton" xmldata))
- method browserNewButton = browserNewButton
- val image191 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image191" ~info:"GtkImage" xmldata))
- method image191 = image191
- val browserBackButton =
+ (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:"BrowserBackButton" ~info:"GtkButton" xmldata))
- method browserBackButton = browserBackButton
- val alignment3 =
+ (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:"alignment3" ~info:"GtkAlignment" xmldata))
- method alignment3 = alignment3
- val hbox6 =
+ (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:"hbox6" ~info:"GtkHBox" xmldata))
- method hbox6 = hbox6
- val image188 =
+ (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:"image188" ~info:"GtkImage" xmldata))
- method image188 = image188
- val label10 =
+ (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:"label10" ~info:"GtkLabel" xmldata))
- method label10 = label10
- val browserForwardButton =
- new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"BrowserForwardButton" ~info:"GtkButton" xmldata))
- method browserForwardButton = browserForwardButton
- val image189 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image189" ~info:"GtkImage" xmldata))
- method image189 = image189
- val browserRefreshButton =
+ (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:"BrowserRefreshButton" ~info:"GtkButton" xmldata))
- method browserRefreshButton = browserRefreshButton
- val image229 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image229" ~info:"GtkImage" xmldata))
- method image229 = image229
- val browserHomeButton =
+ (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:"BrowserHomeButton" ~info:"GtkButton" xmldata))
- method browserHomeButton = browserHomeButton
- val image190 =
- new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image190" ~info:"GtkImage" xmldata))
- method image190 = image190
- val image187 =
+ (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:"image187" ~info:"GtkImage" xmldata))
- method image187 = image187
- val browserUri =
- new GEdit.entry (GtkEdit.Entry.cast
- (Glade.get_widget_msg ~name:"BrowserUri" ~info:"GtkEntry" xmldata))
- method browserUri = browserUri
- val frame1 =
- new GBin.frame (GtkBin.Frame.cast
- (Glade.get_widget_msg ~name:"frame1" ~info:"GtkFrame" xmldata))
- method frame1 = frame1
- val scrolledBrowser =
+ (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:"ScrolledBrowser" ~info:"GtkScrolledWindow" xmldata))
- method scrolledBrowser = scrolledBrowser
+ (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 =
- browserWinEventBox#misc#reparent parent;
+ dialog_vbox3#misc#reparent parent;
toplevel#destroy ()
method check_widgets () = ()
end
let check_all ?(show=false) () =
ignore (GMain.Main.init ());
- let browserWin = new browserWin () in
- if show then browserWin#toplevel#show ();
- browserWin#check_widgets ();
+ let uriChoiceDialog = new uriChoiceDialog () in
+ if show then uriChoiceDialog#toplevel#show ();
+ uriChoiceDialog#check_widgets ();
+ let toolBarWin = new toolBarWin () in
+ if show then toolBarWin#toplevel#show ();
+ toolBarWin#check_widgets ();
let textDialog = new textDialog () in
if show then textDialog#toplevel#show ();
textDialog#check_widgets ();
let scriptWin = new scriptWin () in
if show then scriptWin#toplevel#show ();
scriptWin#check_widgets ();
- let emptyDialog = new emptyDialog () in
- if show then emptyDialog#toplevel#show ();
- emptyDialog#check_widgets ();
+ let mainWin = new mainWin () in
+ if show then mainWin#toplevel#show ();
+ mainWin#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 confirmationDialog = new confirmationDialog () in
- if show then confirmationDialog#toplevel#show ();
- confirmationDialog#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 mainWin = new mainWin () in
- if show then mainWin#toplevel#show ();
- mainWin#check_widgets ();
+ let emptyDialog = new emptyDialog () in
+ if show then emptyDialog#toplevel#show ();
+ emptyDialog#check_widgets ();
+ let confirmationDialog = new confirmationDialog () in
+ if show then confirmationDialog#toplevel#show ();
+ confirmationDialog#check_widgets ();
+ let browserWin = new browserWin () in
+ if show then browserWin#toplevel#show ();
+ browserWin#check_widgets ();
+ let aboutWin = new aboutWin () in
+ if show then aboutWin#toplevel#show ();
+ aboutWin#check_widgets ();
if show then GMain.Main.main ()
;;