]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita.glade
Nicer index for tactics in Yelp.
[helm.git] / matita / matita.glade
index 436dd7b268b664c5cea6a27ebcc6f83b5eb44fb1..71506d55ac3b0f0784755299fd7ba00f36b63135 100644 (file)
                              <accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image856">
+                               <widget class="GtkImage" id="image889">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-new</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image857">
+                               <widget class="GtkImage" id="image890">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-open</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image858">
+                               <widget class="GtkImage" id="image891">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-save</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="s" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image859">
+                               <widget class="GtkImage" id="image892">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-save-as</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="d" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image860">
+                               <widget class="GtkImage" id="image893">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-execute</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image861">
+                               <widget class="GtkImage" id="image894">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-quit</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image862">
+                               <widget class="GtkImage" id="image895">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-undo</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="z" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image863">
+                               <widget class="GtkImage" id="image896">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-redo</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image864">
+                               <widget class="GtkImage" id="image897">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-cut</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image865">
+                               <widget class="GtkImage" id="image898">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-copy</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image866">
+                               <widget class="GtkImage" id="image899">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-paste</property>
                                  <property name="icon_size">1</property>
                              <property name="use_underline">True</property>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image867">
+                               <widget class="GtkImage" id="image900">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-delete</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image868">
+                               <widget class="GtkImage" id="image901">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-find-and-replace</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="plus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image869">
+                               <widget class="GtkImage" id="image902">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-zoom-in</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="minus" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image870">
+                               <widget class="GtkImage" id="image903">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-zoom-out</property>
                                  <property name="icon_size">1</property>
                              <accelerator key="equal" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image871">
+                               <widget class="GtkImage" id="image904">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-zoom-100</property>
                                  <property name="icon_size">1</property>
                      <child>
                        <widget class="GtkMenu" id="helpMenu_menu">
 
+                         <child>
+                           <widget class="GtkImageMenuItem" id="contentsMenuItem">
+                             <property name="visible">True</property>
+                             <property name="label" translatable="yes">_Contents</property>
+                             <property name="use_underline">True</property>
+                             <accelerator key="F1" modifiers="0" signal="activate"/>
+
+                             <child internal-child="image">
+                               <widget class="GtkImage" id="image905">
+                                 <property name="visible">True</property>
+                                 <property name="stock">gtk-help</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="aboutMenuItem">
                              <property name="visible">True</property>
                              <property name="use_underline">True</property>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image872">
+                               <widget class="GtkImage" id="image906">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-about</property>
                                  <property name="icon_size">1</property>