</widget>
</child>
+ <child>
+ <widget class="GtkMenuItem" id="BrowserUrlMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Open _Location ...</property>
+ <property name="use_underline">True</property>
+ <accelerator key="L" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+ </widget>
+ </child>
+
<child>
<widget class="GtkSeparatorMenuItem" id="separatormenuitem1">
<property name="visible">True</property>
<property name="use_underline">True</property>
</widget>
</child>
+
+ <child>
+ <widget class="GtkSeparatorMenuItem" id="separator11">
+ <property name="visible">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="HBugsTutorsMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">HBugs Tutors</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
</widget>
</child>
</widget>
<property name="type">tab</property>
</packing>
</child>
+
+ <child>
+ <widget class="GtkVBox" id="vbox16">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="scrolledwindow13">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+ <property name="shadow_type">GTK_SHADOW_NONE</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTreeView" id="HBugsTutorsList">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="headers_visible">True</property>
+ <property name="rules_hint">False</property>
+ <property name="reorderable">False</property>
+ <property name="enable_search">True</property>
+ <property name="fixed_height_mode">False</property>
+ <property name="hover_selection">False</property>
+ <property name="hover_expand">False</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolbar" id="toolbar3">
+ <property name="visible">True</property>
+ <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem47">
+ <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="HBugsRefreshButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-refresh</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem48">
+ <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="HBugsUnsubscribeButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-remove</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkToolItem" id="toolitem49">
+ <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="HBugsSubscribeButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-add</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="tab_expand">False</property>
+ <property name="tab_fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label29">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">HBugs</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="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+ <property name="width_chars">-1</property>
+ <property name="single_line_mode">False</property>
+ <property name="angle">0</property>
+ </widget>
+ <packing>
+ <property name="type">tab</property>
+ </packing>
+ </child>
</widget>
<packing>
<property name="padding">0</property>
</child>
</widget>
-<widget class="GtkDialog" id="RecordChoiceDialog">
- <property name="width_request">450</property>
- <property name="height_request">400</property>
- <property name="title" translatable="yes">title</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="focus_on_map">True</property>
- <property name="urgency_hint">False</property>
- <property name="has_separator">True</property>
-
- <child internal-child="vbox">
- <widget class="GtkVBox" id="dialog-vbox4">
- <property name="visible">True</property>
- <property name="homogeneous">False</property>
- <property name="spacing">0</property>
-
- <child internal-child="action_area">
- <widget class="GtkHButtonBox" id="dialog-action_area4">
- <property name="visible">True</property>
- <property name="layout_style">GTK_BUTTONBOX_END</property>
-
- <child>
- <widget class="GtkButton" id="RecordChoiceHelpButton">
- <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="RecordChoiceCancelButton">
- <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="RecordChoiceOkButton">
- <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="RecordChoiceDialogLabel">
- <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>
- <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
- <property name="width_chars">-1</property>
- <property name="single_line_mode">False</property>
- <property name="angle">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_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="GtkTreeView" id="RecordChoiceTreeView">
- <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="fixed_height_mode">False</property>
- <property name="hover_selection">False</property>
- <property name="hover_expand">False</property>
- </widget>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">True</property>
- <property name="fill">True</property>
- </packing>
- </child>
- </widget>
- <packing>
- <property name="padding">0</property>
- <property name="expand">True</property>
- <property name="fill">True</property>
- </packing>
- </child>
- </widget>
- </child>
-</widget>
-
<widget class="GtkWindow" id="MainWin">
<property name="title" translatable="yes">Matita</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
</child>
<child>
- <widget class="GtkToolItem" id="toolitemxx">
+ <widget class="GtkToolbar" id="toolbar2">
<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="orientation">GTK_ORIENTATION_VERTICAL</property>
+ <property name="toolbar_style">GTK_TOOLBAR_ICONS</property>
+ <property name="tooltips">True</property>
+ <property name="show_arrow">True</property>
<child>
- <widget class="GtkButton" id="scriptAbortButton">
+ <widget class="GtkToolItem" id="toolitem46">
<property name="visible">True</property>
- <property name="tooltip" translatable="yes">Abort</property>
- <property name="can_focus">True</property>
- <property name="relief">GTK_RELIEF_NONE</property>
- <property name="focus_on_click">True</property>
+ <property name="visible_horizontal">True</property>
+ <property name="visible_vertical">True</property>
+ <property name="is_important">False</property>
<child>
- <widget class="GtkImage" id="image925">
+ <widget class="GtkButton" id="scriptAbortButton">
<property name="visible">True</property>
- <property name="stock">gtk-cancel</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>
- <accessibility>
- <atkproperty name="AtkObject::accessible_name" translatable="yes">abort</atkproperty>
- </accessibility>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NONE</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkImage" id="image927">
+ <property name="visible">True</property>
+ <property name="stock">gtk-stop</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
</widget>
</child>
</widget>
+ <packing>
+ <property name="expand">False</property>
+ <property name="homogeneous">False</property>
+ </packing>
</child>
</widget>
<packing>
<property name="padding">0</property>
<property name="expand">False</property>
- <property name="fill">False</property>
+ <property name="fill">True</property>
</packing>
</child>
</widget>
</child>
</widget>
+<widget class="GtkDialog" id="DisambiguationErrors">
+ <property name="width_request">450</property>
+ <property name="height_request">400</property>
+ <property name="title" translatable="yes">title</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="focus_on_map">True</property>
+ <property name="urgency_hint">False</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="vbox14">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child internal-child="action_area">
+ <widget class="GtkHButtonBox" id="hbuttonbox2">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="button6">
+ <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="disambiguationErrorsMoreErrors">
+ <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">-6</property>
+
+ <child>
+ <widget class="GtkAlignment" id="alignment18">
+ <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="hbox29">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
+
+ <child>
+ <widget class="GtkImage" id="image926">
+ <property name="visible">True</property>
+ <property name="stock">gtk-zoom-in</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="label28">
+ <property name="visible">True</property>
+ <property name="label">More</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>
+ <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+ <property name="width_chars">-1</property>
+ <property name="single_line_mode">False</property>
+ <property name="angle">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="disambiguationErrorsCancelButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="has_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="disambiguationErrorsOkButton">
+ <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="vbox15">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkLabel" id="disambiguationErrorsLabel">
+ <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>
+ <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+ <property name="width_chars">-1</property>
+ <property name="single_line_mode">False</property>
+ <property name="angle">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="scrolledwindow12">
+ <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="GtkTreeView" id="treeview">
+ <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="fixed_height_mode">False</property>
+ <property name="hover_selection">False</property>
+ <property name="hover_expand">False</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
</glade-interface>