]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matita.glade
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
New menus Undo/Redo (bugged), Cut/Copy/Paste/Delete.
[helm.git] / helm / matita / matita.glade
diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 68fecc5b5c82b5eaf75da3d81ad9be98ed8f4144..2fb05862dab6d602668568a8275b928374deea1c 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -881,7 +881,7 @@ Copyright (C) 2005,
                              <property name="use_underline">True</property>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image384">
+                               <widget class="GtkImage" id="image402">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-new</property>
                                  <property name="icon_size">1</property>
@@ -902,7 +902,7 @@ Copyright (C) 2005,
                              <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image385">
+                               <widget class="GtkImage" id="image403">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-open</property>
                                  <property name="icon_size">1</property>
@@ -923,7 +923,7 @@ Copyright (C) 2005,
                              <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image386">
+                               <widget class="GtkImage" id="image404">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-save</property>
                                  <property name="icon_size">1</property>
@@ -943,7 +943,7 @@ Copyright (C) 2005,
                              <property name="use_underline">True</property>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image387">
+                               <widget class="GtkImage" id="image405">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-save-as</property>
                                  <property name="icon_size">1</property>
@@ -964,7 +964,7 @@ Copyright (C) 2005,
                              <accelerator key="d" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image388">
+                               <widget class="GtkImage" id="image406">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-execute</property>
                                  <property name="icon_size">1</property>
@@ -991,7 +991,7 @@ Copyright (C) 2005,
                              <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image389">
+                               <widget class="GtkImage" id="image407">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-quit</property>
                                  <property name="icon_size">1</property>
@@ -1017,6 +1017,145 @@ Copyright (C) 2005,
                      <child>
                        <widget class="GtkMenu" id="editMenu_menu">
 
+                         <child>
+                           <widget class="GtkImageMenuItem" id="undoMenuItem">
+                             <property name="visible">True</property>
+                             <property name="sensitive">False</property>
+                             <property name="label" translatable="yes">Undo</property>
+                             <property name="use_underline">True</property>
+                             <accelerator key="z" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+                             <child internal-child="image">
+                               <widget class="GtkImage" id="image408">
+                                 <property name="visible">True</property>
+                                 <property name="stock">gtk-undo</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="redoMenuItem">
+                             <property name="visible">True</property>
+                             <property name="sensitive">False</property>
+                             <property name="label" translatable="yes">Redo</property>
+                             <property name="use_underline">True</property>
+                             <accelerator key="z" modifiers="GDK_CONTROL_MASK | GDK_SHIFT_MASK" signal="activate"/>
+
+                             <child internal-child="image">
+                               <widget class="GtkImage" id="image409">
+                                 <property name="visible">True</property>
+                                 <property name="stock">gtk-redo</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="separator3">
+                             <property name="visible">True</property>
+                           </widget>
+                         </child>
+
+                         <child>
+                           <widget class="GtkImageMenuItem" id="cutMenuItem">
+                             <property name="visible">True</property>
+                             <property name="label" translatable="yes">Cut</property>
+                             <property name="use_underline">True</property>
+                             <accelerator key="x" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+                             <child internal-child="image">
+                               <widget class="GtkImage" id="image410">
+                                 <property name="visible">True</property>
+                                 <property name="stock">gtk-cut</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="copyMenuItem">
+                             <property name="visible">True</property>
+                             <property name="label" translatable="yes">Copy</property>
+                             <property name="use_underline">True</property>
+                             <accelerator key="c" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+                             <child internal-child="image">
+                               <widget class="GtkImage" id="image411">
+                                 <property name="visible">True</property>
+                                 <property name="stock">gtk-copy</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="pasteMenuItem">
+                             <property name="visible">True</property>
+                             <property name="label" translatable="yes">Paste</property>
+                             <property name="use_underline">True</property>
+                             <accelerator key="v" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+                             <child internal-child="image">
+                               <widget class="GtkImage" id="image412">
+                                 <property name="visible">True</property>
+                                 <property name="stock">gtk-paste</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="deleteMenuItem">
+                             <property name="visible">True</property>
+                             <property name="label" translatable="yes">Delete</property>
+                             <property name="use_underline">True</property>
+
+                             <child internal-child="image">
+                               <widget class="GtkImage" id="image413">
+                                 <property name="visible">True</property>
+                                 <property name="stock">gtk-delete</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="separator4">
+                             <property name="visible">True</property>
+                           </widget>
+                         </child>
+
                          <child>
                            <widget class="GtkImageMenuItem" id="findReplMenuItem">
                              <property name="visible">True</property>
@@ -1025,7 +1164,7 @@ Copyright (C) 2005,
                              <accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
 
                              <child internal-child="image">
-                               <widget class="GtkImage" id="image390">
+                               <widget class="GtkImage" id="image414">
                                  <property name="visible">True</property>
                                  <property name="stock">gtk-find-and-replace</property>
                                  <property name="icon_size">1</property>
@@ -1071,6 +1210,12 @@ Copyright (C) 2005,
                            </widget>
                          </child>
 
+                         <child>
+                           <widget class="GtkSeparatorMenuItem" id="separator5">
+                             <property name="visible">True</property>
+                           </widget>
+                         </child>
+
                          <child>
                            <widget class="GtkCheckMenuItem" id="fullscreenMenuItem">
                              <property name="visible">True</property>
Unnamed repository; edit this file 'description' to name the repository.