filled toolbar and implemented buttons behaviours

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 7c272a828deac347d774ce49b915faa8d33af56d..4ecd6d46a705389b0a20b9d06af9a3309826c0e7 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -449,10 +449,10 @@
 </widget>
 
 <widget class="GtkWindow" id="ToolBarWin">
-  <property name="width_request">130</property>
+  <property name="width_request">150</property>
   <property name="height_request">450</property>
   <property name="visible">True</property>
-  <property name="title" translatable="yes">ToolBar</property>
+  <property name="title" translatable="yes">Tactics</property>
   <property name="type">GTK_WINDOW_TOPLEVEL</property>
   <property name="window_position">GTK_WIN_POS_NONE</property>
   <property name="modal">False</property>
@@ -471,86 +471,524 @@
       <property name="above_child">False</property>
 
       <child>
-       <widget class="GtkVBox" id="vbox1">
+       <widget class="GtkVBox" id="ToolBarVBox">
          <property name="visible">True</property>
          <property name="homogeneous">False</property>
          <property name="spacing">0</property>
 
          <child>
-           <widget class="GtkVButtonBox" id="vbuttonbox1">
+           <widget class="GtkToolbar" id="toolbar2">
              <property name="visible">True</property>
-             <property name="layout_style">GTK_BUTTONBOX_DEFAULT_STYLE</property>
-             <property name="spacing">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="GtkButton" id="button1">
-                 <property name="width_request">120</property>
+               <widget class="GtkToolItem" id="toolitem4">
                  <property name="visible">True</property>
-                 <property name="can_default">True</property>
-                 <property name="can_focus">True</property>
-                 <property name="label" translatable="yes">button1</property>
-                 <property name="use_underline">True</property>
-                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                 <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="GtkButton" id="introsButton">
+                     <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="GtkButton" id="button2">
+               <widget class="GtkToolItem" id="toolitem5">
                  <property name="visible">True</property>
-                 <property name="can_default">True</property>
-                 <property name="can_focus">True</property>
-                 <property name="label" translatable="yes">button2</property>
-                 <property name="use_underline">True</property>
-                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                 <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="GtkButton" id="applyButton">
+                     <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="button3">
+               <widget class="GtkToolItem" id="toolitem6">
                  <property name="visible">True</property>
-                 <property name="can_default">True</property>
-                 <property name="can_focus">True</property>
-                 <property name="label" translatable="yes">button3</property>
-                 <property name="use_underline">True</property>
-                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                 <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="GtkButton" id="exactButton">
+                     <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="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="GtkButton" id="button4">
+               <widget class="GtkToolItem" id="toolitem7">
                  <property name="visible">True</property>
-                 <property name="can_default">True</property>
-                 <property name="can_focus">True</property>
-                 <property name="label" translatable="yes">button4</property>
-                 <property name="use_underline">True</property>
-                 <property name="relief">GTK_RELIEF_NORMAL</property>
-                 <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="GtkButton" id="elimButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">Elim</property>
+                     <property name="can_focus">True</property>
+                     <property name="label" translatable="yes">elim</property>
+                     <property name="use_underline">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+                   </widget>
+                 </child>
                </widget>
+               <packing>
+                 <property name="expand">False</property>
+                 <property name="homogeneous">False</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkToolItem" id="toolitem8">
+                 <property name="visible">True</property>
+                 <property name="visible_horizontal">True</property>
+                 <property name="visible_vertical">True</property>
+                 <property name="is_important">False</property>
+
+                 <child>
+                   <widget class="GtkButton" id="elimTypeButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">ElimType</property>
+                     <property name="can_focus">True</property>
+                     <property name="label" translatable="yes">elimTy</property>
+                     <property name="use_underline">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="expand">False</property>
+                 <property name="homogeneous">False</property>
+               </packing>
              </child>
            </widget>
            <packing>
              <property name="padding">0</property>
              <property name="expand">False</property>
-             <property name="fill">True</property>
+             <property name="fill">False</property>
            </packing>
          </child>
 
          <child>
-           <widget class="GtkHSeparator" id="hseparator1">
+           <widget class="GtkToolbar" id="toolbar4">
              <property name="visible">True</property>
+             <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+             <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+             <property name="tooltips">True</property>
+             <property name="show_arrow">True</property>
+
+             <child>
+               <widget class="GtkToolItem" id="toolitem9">
+                 <property name="visible">True</property>
+                 <property name="visible_horizontal">True</property>
+                 <property name="visible_vertical">True</property>
+                 <property name="is_important">False</property>
+
+                 <child>
+                   <widget class="GtkButton" id="splitButton">
+                     <property name="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>
+
+             <child>
+               <widget class="GtkToolItem" id="toolitem10">
+                 <property name="visible">True</property>
+                 <property name="visible_horizontal">True</property>
+                 <property name="visible_vertical">True</property>
+                 <property name="is_important">False</property>
+
+                 <child>
+                   <widget class="GtkButton" id="leftButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">Left</property>
+                     <property name="can_focus">True</property>
+                     <property name="label" translatable="yes">left</property>
+                     <property name="use_underline">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="expand">False</property>
+                 <property name="homogeneous">False</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkToolItem" id="toolitem11">
+                 <property name="visible">True</property>
+                 <property name="visible_horizontal">True</property>
+                 <property name="visible_vertical">True</property>
+                 <property name="is_important">False</property>
+
+                 <child>
+                   <widget class="GtkButton" id="rightButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">Right</property>
+                     <property name="can_focus">True</property>
+                     <property name="label" translatable="yes">right</property>
+                     <property name="use_underline">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="expand">False</property>
+                 <property name="homogeneous">False</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkToolItem" id="toolitem12">
+                 <property name="visible">True</property>
+                 <property name="visible_horizontal">True</property>
+                 <property name="visible_vertical">True</property>
+                 <property name="is_important">False</property>
+
+                 <child>
+                   <widget class="GtkButton" id="existsButton">
+                     <property name="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">5</property>
+             <property name="padding">0</property>
              <property name="expand">False</property>
-             <property name="fill">True</property>
+             <property name="fill">False</property>
            </packing>
          </child>
 
          <child>
-           <placeholder/>
+           <widget class="GtkToolbar" id="toolbar5">
+             <property name="visible">True</property>
+             <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+             <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+             <property name="tooltips">True</property>
+             <property name="show_arrow">True</property>
+
+             <child>
+               <widget class="GtkToolItem" id="toolitem14">
+                 <property name="visible">True</property>
+                 <property name="visible_horizontal">True</property>
+                 <property name="visible_vertical">True</property>
+                 <property name="is_important">False</property>
+
+                 <child>
+                   <widget class="GtkButton" id="reflexivityButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">Reflexivity</property>
+                     <property name="can_focus">True</property>
+                     <property name="label" translatable="yes">refl</property>
+                     <property name="use_underline">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="expand">False</property>
+                 <property name="homogeneous">False</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkToolItem" id="toolitem15">
+                 <property name="visible">True</property>
+                 <property name="visible_horizontal">True</property>
+                 <property name="visible_vertical">True</property>
+                 <property name="is_important">False</property>
+
+                 <child>
+                   <widget class="GtkButton" id="symmetryButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">Symmetry</property>
+                     <property name="can_focus">True</property>
+                     <property name="label" translatable="yes">sym</property>
+                     <property name="use_underline">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="expand">False</property>
+                 <property name="homogeneous">False</property>
+               </packing>
+             </child>
+
+             <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="visible">True</property>
+                     <property name="tooltip" translatable="yes">Transitivity</property>
+                     <property name="can_focus">True</property>
+                     <property name="label" translatable="yes">trans</property>
+                     <property name="use_underline">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="expand">False</property>
+                 <property name="homogeneous">False</property>
+               </packing>
+             </child>
+           </widget>
+           <packing>
+             <property name="padding">0</property>
+             <property name="expand">False</property>
+             <property name="fill">False</property>
+           </packing>
+         </child>
+
+         <child>
+           <widget class="GtkToolbar" id="toolbar6">
+             <property name="visible">True</property>
+             <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+             <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+             <property name="tooltips">True</property>
+             <property name="show_arrow">True</property>
+
+             <child>
+               <widget class="GtkToolItem" id="toolitem17">
+                 <property name="visible">True</property>
+                 <property name="visible_horizontal">True</property>
+                 <property name="visible_vertical">True</property>
+                 <property name="is_important">False</property>
+
+                 <child>
+                   <widget class="GtkButton" id="assumptionButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">Assumption</property>
+                     <property name="can_focus">True</property>
+                     <property name="label" translatable="yes">assum</property>
+                     <property name="use_underline">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="expand">False</property>
+                 <property name="homogeneous">False</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkToolItem" id="toolitem18">
+                 <property name="visible">True</property>
+                 <property name="visible_horizontal">True</property>
+                 <property name="visible_vertical">True</property>
+                 <property name="is_important">False</property>
+
+                 <child>
+                   <widget class="GtkButton" id="searchButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">Search</property>
+                     <property name="can_focus">True</property>
+                     <property name="label" translatable="yes">search</property>
+                     <property name="use_underline">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="expand">False</property>
+                 <property name="homogeneous">False</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkToolItem" id="toolitem19">
+                 <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="visible">True</property>
+                     <property name="tooltip" translatable="yes">Auto</property>
+                     <property name="can_focus">True</property>
+                     <property name="label" translatable="yes">auto</property>
+                     <property name="use_underline">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="expand">False</property>
+                 <property name="homogeneous">False</property>
+               </packing>
+             </child>
+           </widget>
+           <packing>
+             <property name="padding">0</property>
+             <property name="expand">False</property>
+             <property name="fill">False</property>
+           </packing>
+         </child>
+
+         <child>
+           <widget class="GtkToolbar" id="toolbar7">
+             <property name="visible">True</property>
+             <property name="orientation">GTK_ORIENTATION_HORIZONTAL</property>
+             <property name="toolbar_style">GTK_TOOLBAR_BOTH</property>
+             <property name="tooltips">True</property>
+             <property name="show_arrow">True</property>
+
+             <child>
+               <widget class="GtkToolItem" id="toolitem20">
+                 <property name="visible">True</property>
+                 <property name="visible_horizontal">True</property>
+                 <property name="visible_vertical">True</property>
+                 <property name="is_important">False</property>
+
+                 <child>
+                   <widget class="GtkButton" id="cutButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">Cut</property>
+                     <property name="can_focus">True</property>
+                     <property name="label" translatable="yes">cut</property>
+                     <property name="use_underline">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="expand">False</property>
+                 <property name="homogeneous">False</property>
+               </packing>
+             </child>
+
+             <child>
+               <widget class="GtkToolItem" id="toolitem21">
+                 <property name="visible">True</property>
+                 <property name="visible_horizontal">True</property>
+                 <property name="visible_vertical">True</property>
+                 <property name="is_important">False</property>
+
+                 <child>
+                   <widget class="GtkButton" id="replaceButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">Replace</property>
+                     <property name="can_focus">True</property>
+                     <property name="label" translatable="yes">repl</property>
+                     <property name="use_underline">True</property>
+                     <property name="relief">GTK_RELIEF_NORMAL</property>
+                     <property name="focus_on_click">True</property>
+                   </widget>
+                 </child>
+               </widget>
+               <packing>
+                 <property name="expand">False</property>
+                 <property name="homogeneous">False</property>
+               </packing>
+             </child>
+           </widget>
+           <packing>
+             <property name="padding">0</property>
+             <property name="expand">False</property>
+             <property name="fill">False</property>
+           </packing>
          </child>
        </widget>
       </child>
@@ -1464,4 +1902,123 @@ Copyright (C) 2004,
   </child>
 </widget>
 
+<widget class="GtkDialog" id="TextDialog">
+  <property name="title" translatable="yes">DUMMY</property>
+  <property name="type">GTK_WINDOW_TOPLEVEL</property>
+  <property name="window_position">GTK_WIN_POS_NONE</property>
+  <property name="modal">False</property>
+  <property name="resizable">True</property>
+  <property name="destroy_with_parent">False</property>
+  <property name="decorated">True</property>
+  <property name="skip_taskbar_hint">False</property>
+  <property name="skip_pager_hint">False</property>
+  <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+  <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+  <property name="has_separator">True</property>
+
+  <child internal-child="vbox">
+    <widget class="GtkVBox" id="vbox5">
+      <property name="visible">True</property>
+      <property name="homogeneous">False</property>
+      <property name="spacing">0</property>
+
+      <child internal-child="action_area">
+       <widget class="GtkHButtonBox" id="hbuttonbox1">
+         <property name="visible">True</property>
+         <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+         <child>
+           <widget class="GtkButton" id="TextDialogCancelButton">
+             <property name="visible">True</property>
+             <property name="can_default">True</property>
+             <property name="can_focus">True</property>
+             <property name="label">gtk-cancel</property>
+             <property name="use_stock">True</property>
+             <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
+             <property name="response_id">-6</property>
+           </widget>
+         </child>
+
+         <child>
+           <widget class="GtkButton" id="TextDialogOkButton">
+             <property name="visible">True</property>
+             <property name="can_default">True</property>
+             <property name="can_focus">True</property>
+             <property name="label">gtk-ok</property>
+             <property name="use_stock">True</property>
+             <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="focus_on_click">True</property>
+             <property name="response_id">-5</property>
+           </widget>
+         </child>
+       </widget>
+       <packing>
+         <property name="padding">0</property>
+         <property name="expand">False</property>
+         <property name="fill">True</property>
+         <property name="pack_type">GTK_PACK_END</property>
+       </packing>
+      </child>
+
+      <child>
+       <widget class="GtkLabel" id="TextDialogLabel">
+         <property name="visible">True</property>
+         <property name="label" translatable="yes">DUMMY</property>
+         <property name="use_underline">False</property>
+         <property name="use_markup">False</property>
+         <property name="justify">GTK_JUSTIFY_LEFT</property>
+         <property name="wrap">False</property>
+         <property name="selectable">False</property>
+         <property name="xalign">0.5</property>
+         <property name="yalign">0.5</property>
+         <property name="xpad">0</property>
+         <property name="ypad">0</property>
+       </widget>
+       <packing>
+         <property name="padding">0</property>
+         <property name="expand">False</property>
+         <property name="fill">False</property>
+       </packing>
+      </child>
+
+      <child>
+       <widget class="GtkScrolledWindow" id="scrolledwindow2">
+         <property name="visible">True</property>
+         <property name="can_focus">True</property>
+         <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+         <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+         <property name="shadow_type">GTK_SHADOW_IN</property>
+         <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+         <child>
+           <widget class="GtkTextView" id="TextDialogTextView">
+             <property name="visible">True</property>
+             <property name="can_focus">True</property>
+             <property name="editable">True</property>
+             <property name="overwrite">False</property>
+             <property name="accepts_tab">True</property>
+             <property name="justification">GTK_JUSTIFY_LEFT</property>
+             <property name="wrap_mode">GTK_WRAP_NONE</property>
+             <property name="cursor_visible">True</property>
+             <property name="pixels_above_lines">0</property>
+             <property name="pixels_below_lines">0</property>
+             <property name="pixels_inside_wrap">0</property>
+             <property name="left_margin">0</property>
+             <property name="right_margin">0</property>
+             <property name="indent">0</property>
+             <property name="text" translatable="yes"></property>
+           </widget>
+         </child>
+       </widget>
+       <packing>
+         <property name="padding">0</property>
+         <property name="expand">True</property>
+         <property name="fill">True</property>
+       </packing>
+      </child>
+    </widget>
+  </child>
+</widget>
+
 </glade-interface>

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 2619b9bb9968e5c20631bbe64523f7fd7feb6a9c..e565c03a787e6f0c1cd6b4eaaef9afba9b1048cf 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -127,6 +127,14 @@ let interpreter =
   let console = gui#console in
   new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console ()
 
+  (** prompt the user for the textual input of a term and disambiguate it *)
+let ask_term ?(title = "term input") ?(msg = "insert term") () =
+  match gui#askText ~title ~msg () with
+  | Some t ->
+      let (_, _, term) = disambiguator#disambiguateTerm (Stream.of_string t) in
+      Some term
+  | None -> None
+
 let _ =
   gui#setQuitCallback quit;
   gui#setPhraseCallback interpreter#evalPhrase;
@@ -155,7 +163,36 @@ let _ =
     | Some f ->
         gui#console#echo_error (sprintf
           "Don't know what to do with file: %s\nUnrecognized file format."
-          f)))
+          f)));
+  let tac_w_term name tac _ =
+    match ask_term ~title:name ~msg:("term for " ^ name) () with
+    | Some term -> (get_proof ())#apply_tactic (tac ~term)
+    | None -> ()
+  in
+  let tac _ tac _ = (get_proof ())#apply_tactic tac in
+  let tbar = gui#toolbar in
+  ignore (tbar#introsButton#connect#clicked (tac "intros" (Tactics.intros ())));
+  ignore (tbar#applyButton#connect#clicked (tac_w_term "apply" Tactics.apply));
+  ignore (tbar#exactButton#connect#clicked (tac_w_term "exact" Tactics.exact));
+  ignore (tbar#elimButton#connect#clicked (tac_w_term "elim"
+    Tactics.elim_intros_simpl));
+  ignore (tbar#elimTypeButton#connect#clicked (tac_w_term "elim type"
+    Tactics.elim_type));
+  ignore (tbar#splitButton#connect#clicked (tac "split" Tactics.split));
+  ignore (tbar#leftButton#connect#clicked (tac "left" Tactics.left));
+  ignore (tbar#rightButton#connect#clicked (tac "right" Tactics.right));
+  ignore (tbar#existsButton#connect#clicked (tac "exists" Tactics.exists));
+  ignore (tbar#reflexivityButton#connect#clicked (tac "reflexivity"
+    Tactics.reflexivity));
+  ignore (tbar#symmetryButton#connect#clicked (tac "symmetry"
+    Tactics.symmetry));
+  ignore (tbar#transitivityButton#connect#clicked (tac_w_term "transitivity"
+    Tactics.transitivity));
+  ignore (tbar#assumptionButton#connect#clicked (tac "assumption"
+    Tactics.assumption));
+  ignore (tbar#cutButton#connect#clicked (tac_w_term "cut"
+    (Tactics.cut ?mk_fresh_name_callback:None)));
+  ignore (tbar#autoButton#connect#clicked (tac "auto" (Tactics.auto ~dbd)))
 
   (** <DEBUGGING> *)
 

diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml
index cb72003911751663dc69a2441870910f25f20a79..95ae9648ea7b90316454cc9f2fa3fbf9fed48947 100644 (file)
--- a/helm/matita/matitaGeneratedGui.ml
+++ b/helm/matita/matitaGeneratedGui.ml
@@ -236,30 +236,102 @@ class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GBin.event_box (GtkBin.EventBox.cast
         (Glade.get_widget_msg ~name:"ToolBarEventBox" ~info:"GtkEventBox" xmldata))
     method toolBarEventBox = toolBarEventBox
-    val vbox1 =
+    val toolBarVBox =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"vbox1" ~info:"GtkVBox" xmldata))
-    method vbox1 = vbox1
-    val vbuttonbox1 =
-      new GPack.button_box (GtkPack.BBox.cast
-        (Glade.get_widget_msg ~name:"vbuttonbox1" ~info:"GtkVButtonBox" xmldata))
-    method vbuttonbox1 = vbuttonbox1
-    val button1 =
+        (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:"button1" ~info:"GtkButton" xmldata))
-    method button1 = button1
-    val button2 =
+        (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:"button2" ~info:"GtkButton" xmldata))
-    method button2 = button2
-    val button3 =
+        (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:"button3" ~info:"GtkButton" xmldata))
-    method button3 = button3
-    val button4 =
+        (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 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 searchButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"searchButton" ~info:"GtkButton" xmldata))
+    method searchButton = searchButton
+    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:"button4" ~info:"GtkButton" xmldata))
-    method button4 = button4
+        (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 ()
@@ -604,9 +676,57 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       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
 
 let check_all ?(show=false) () =
   ignore (GMain.Main.init ());
+  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 ();

diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli
index 3c646b10cbaadf32efe9d3174ba7eb69751e8b57..d8e34fca358862271b5674971cc1e0d62267aa0b 100644 (file)
--- a/helm/matita/matitaGeneratedGui.mli
+++ b/helm/matita/matitaGeneratedGui.mli
@@ -137,28 +137,64 @@ class toolBarWin :
   ?autoconnect:bool ->
   unit ->
   object
-    val button1 : GButton.button
-    val button2 : GButton.button
-    val button3 : GButton.button
-    val button4 : GButton.button
+    val applyButton : GButton.button
+    val assumptionButton : GButton.button
+    val autoButton : GButton.button
+    val cutButton : GButton.button
+    val elimButton : GButton.button
+    val elimTypeButton : GButton.button
+    val exactButton : GButton.button
+    val existsButton : GButton.button
+    val introsButton : GButton.button
+    val leftButton : GButton.button
+    val reflexivityButton : GButton.button
+    val replaceButton : GButton.button
+    val rightButton : GButton.button
+    val searchButton : GButton.button
+    val splitButton : GButton.button
+    val symmetryButton : GButton.button
     val toolBarEventBox : GBin.event_box
+    val toolBarVBox : GPack.box
     val toolBarWin : GWindow.window
+    val toolbar2 : GButton.toolbar
+    val toolbar3 : GButton.toolbar
+    val toolbar4 : GButton.toolbar
+    val toolbar5 : GButton.toolbar
+    val toolbar6 : GButton.toolbar
+    val toolbar7 : GButton.toolbar
     val toplevel : GWindow.window
-    val vbox1 : GPack.box
-    val vbuttonbox1 : GPack.button_box
+    val transitivityButton : GButton.button
     val xml : Glade.glade_xml Gtk.obj
+    method applyButton : GButton.button
+    method assumptionButton : GButton.button
+    method autoButton : GButton.button
     method bind : name:string -> callback:(unit -> unit) -> unit
-    method button1 : GButton.button
-    method button2 : GButton.button
-    method button3 : GButton.button
-    method button4 : GButton.button
     method check_widgets : unit -> unit
+    method cutButton : GButton.button
+    method elimButton : GButton.button
+    method elimTypeButton : GButton.button
+    method exactButton : GButton.button
+    method existsButton : GButton.button
+    method introsButton : GButton.button
+    method leftButton : GButton.button
+    method reflexivityButton : GButton.button
     method reparent : GObj.widget -> unit
+    method replaceButton : GButton.button
+    method rightButton : GButton.button
+    method searchButton : GButton.button
+    method splitButton : GButton.button
+    method symmetryButton : GButton.button
     method toolBarEventBox : GBin.event_box
+    method toolBarVBox : GPack.box
     method toolBarWin : GWindow.window
+    method toolbar2 : GButton.toolbar
+    method toolbar3 : GButton.toolbar
+    method toolbar4 : GButton.toolbar
+    method toolbar5 : GButton.toolbar
+    method toolbar6 : GButton.toolbar
+    method toolbar7 : GButton.toolbar
     method toplevel : GWindow.window
-    method vbox1 : GPack.box
-    method vbuttonbox1 : GPack.button_box
+    method transitivityButton : GButton.button
     method xml : Glade.glade_xml Gtk.obj
   end
 class confirmationDialog :
@@ -383,4 +419,34 @@ class scriptWin :
     method vbox4 : GPack.box
     method xml : Glade.glade_xml Gtk.obj
   end
+class textDialog :
+  ?file:string ->
+  ?domain:string ->
+  ?autoconnect:bool ->
+  unit ->
+  object
+    val hbuttonbox1 : GPack.button_box
+    val scrolledwindow2 : GBin.scrolled_window
+    val textDialog : GWindow.dialog_any
+    val textDialogCancelButton : GButton.button
+    val textDialogLabel : GMisc.label
+    val textDialogOkButton : GButton.button
+    val textDialogTextView : GText.view
+    val toplevel : GWindow.dialog_any
+    val vbox5 : GPack.box
+    val xml : Glade.glade_xml Gtk.obj
+    method bind : name:string -> callback:(unit -> unit) -> unit
+    method check_widgets : unit -> unit
+    method hbuttonbox1 : GPack.button_box
+    method reparent : GObj.widget -> unit
+    method scrolledwindow2 : GBin.scrolled_window
+    method textDialog : GWindow.dialog_any
+    method textDialogCancelButton : GButton.button
+    method textDialogLabel : GMisc.label
+    method textDialogOkButton : GButton.button
+    method textDialogTextView : GText.view
+    method toplevel : GWindow.dialog_any
+    method vbox5 : GPack.box
+    method xml : Glade.glade_xml Gtk.obj
+  end
 val check_all : ?show:bool -> unit -> unit

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 6b70a498f05e43bd9b93d6f09b13cd7661683e08..d50a2f31964d5fe50865e9c24e674abf0672488a 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -164,6 +164,26 @@ class gui file =
       GtkThread.main ();
       chosen_file
 
+    method askText ?(title = "") ?(msg = "") () =
+      let dialog = new textDialog () in
+      dialog#textDialog#set_title title;
+      dialog#textDialogLabel#set_label msg;
+      let text = ref None in
+      let return v =
+        text := v;
+        dialog#textDialog#destroy ();
+        GMain.Main.quit ()
+      in
+      ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
+      ignore (dialog#textDialogCancelButton#connect#clicked (fun _ ->
+        return None));
+      ignore (dialog#textDialogOkButton#connect#clicked (fun _ ->
+        let text = dialog#textDialogTextView#buffer#get_text () in
+        return (Some text)));
+      dialog#textDialog#show ();
+      GtkThread.main ();
+      !text
+
   end
 
 let instance =

diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli
index a185aaf740fbee8315deaa62eacdb110b0fec76e..a74403fdb854dfaead2ba3f87f60c9d0134e4f7d 100644 (file)
--- a/helm/matita/matitaGui.mli
+++ b/helm/matita/matitaGui.mli
@@ -63,6 +63,7 @@ class gui :
     method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog
 
     method chooseFile: unit -> string option
+    method askText: ?title:string -> ?msg:string -> unit -> string option
 
   end
 

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 17a055174d91507fdd60c9b6f15a8b2af7b21f48..d5ca65d22bebddf4dddaf3aa131bc807e1703b93 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -188,28 +188,26 @@ class proofState
     | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic
     | TacticAst.Intros (_, names) ->  (* TODO Zack implement intros length *)
         PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
-    | TacticAst.Reflexivity -> EqualityTactics.reflexivity_tac
-    | TacticAst.Assumption -> VariousTactics.assumption_tac
-    | TacticAst.Contradiction -> NegationTactics.contradiction_tac
-    | TacticAst.Exists -> IntroductionTactics.exists_tac
-    | TacticAst.Fourier -> FourierR.fourier_tac
-    | TacticAst.Left -> IntroductionTactics.left_tac
-    | TacticAst.Right -> IntroductionTactics.right_tac
-    | TacticAst.Ring -> Ring.ring_tac
-    | TacticAst.Split -> IntroductionTactics.split_tac
-    | TacticAst.Symmetry -> EqualityTactics.symmetry_tac
-    | TacticAst.Transitivity term ->
-        EqualityTactics.transitivity_tac (disambiguate term)
-    | TacticAst.Apply term -> PrimitiveTactics.apply_tac (disambiguate term)
-    | TacticAst.Absurd term -> NegationTactics.absurd_tac (disambiguate term)
-    | TacticAst.Exact term -> PrimitiveTactics.exact_tac (disambiguate term)
-    | TacticAst.Cut term -> PrimitiveTactics.cut_tac (disambiguate term)
+    | TacticAst.Reflexivity -> Tactics.reflexivity
+    | TacticAst.Assumption -> Tactics.assumption
+    | TacticAst.Contradiction -> Tactics.contradiction
+    | TacticAst.Exists -> Tactics.exists
+    | TacticAst.Fourier -> Tactics.fourier
+    | TacticAst.Left -> Tactics.left
+    | TacticAst.Right -> Tactics.right
+    | TacticAst.Ring -> Tactics.ring
+    | TacticAst.Split -> Tactics.split
+    | TacticAst.Symmetry -> Tactics.symmetry
+    | TacticAst.Transitivity term -> Tactics.transitivity (disambiguate term)
+    | TacticAst.Apply term -> Tactics.apply (disambiguate term)
+    | TacticAst.Absurd term -> Tactics.absurd (disambiguate term)
+    | TacticAst.Exact term -> Tactics.exact (disambiguate term)
+    | TacticAst.Cut term -> Tactics.cut (disambiguate term)
     | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
-        PrimitiveTactics.elim_intros_simpl_tac (disambiguate term)
-    | TacticAst.ElimType term ->
-        EliminationTactics.elim_type_tac (disambiguate term)
+        Tactics.elim_intros_simpl (disambiguate term)
+    | TacticAst.ElimType term -> Tactics.elim_type (disambiguate term)
     | TacticAst.Replace (what, with_what) ->
-        EqualityTactics.replace_tac ~what:(disambiguate what)
+        Tactics.replace ~what:(disambiguate what)
           ~with_what:(disambiguate with_what)
   (*
     (* TODO Zack a lot more of tactics to be implemented here ... *)