New menus Undo/Redo (bugged), Cut/Copy/Paste/Delete.

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>

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 92626557c11550148ccb4eb6485bb8e05cf3f5c1..2af7046457d42ab3ad9ec4c6b57e58739000320a 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -60,7 +60,6 @@ TODO
     su bisognerebbe tornare su di un passo e non fare undo degli alias
     (Zack: nella history ci sono anche gli offset per sapere a che pezzo di
     script uno stato appartiene)
-  - Implementare menu edit: cut/copy/undo/etc.
   - keybinding globali: CTRL-{su,giu,...} devono fungere anche quando altre
     finestre hanno il focus (e.g. cicBrowser). C'e' gia' da qualche parte il
     codice che aggiunge i keybinding a tutte le eventBox, e' da ripristinare
@@ -87,6 +86,7 @@ TODO
   - non chiudere transitivamente i moo ?? 
 
 DONE
+- Implementare menu edit: cut/copy/undo/etc. -> CSC
 - gestione dei path per include: il path deve essere assoluto? da decidere ...
   ( -I ?? o chiedere a matitamake la root e farci una find? ) -> Gares
 - freeze durante avanzamento -> Gares, CSC

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index ac69d2615a902bc822ff656a8a4dcbe543a289a0..78fbf2f2f25546394dc95b85ff4da5ff8f56c978 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -197,6 +197,27 @@ class gui () =
       connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ());
       ignore(findRepl#toplevel#event#connect#delete 
         ~callback:(fun _ -> hide_find_Repl ();true));
+      ignore(self#main#undoMenuItem#connect#activate
+        ~callback:source_view#source_buffer#undo);
+      ignore(source_view#source_buffer#connect#can_undo
+        ~callback:self#main#undoMenuItem#misc#set_sensitive);
+      ignore(self#main#redoMenuItem#connect#activate
+        ~callback:source_view#source_buffer#redo);
+      ignore(source_view#source_buffer#connect#can_redo
+        ~callback:self#main#redoMenuItem#misc#set_sensitive);
+      let clipboard =
+       let atom = Gdk.Atom.clipboard in
+        GData.clipboard atom in
+      ignore(self#main#cutMenuItem#connect#activate
+        ~callback:(fun () -> source_view#buffer#cut_clipboard clipboard));
+      ignore(self#main#copyMenuItem#connect#activate
+        ~callback:(fun () -> source_view#buffer#copy_clipboard clipboard));
+      ignore(self#main#pasteMenuItem#connect#activate
+        ~callback:(fun () ->
+          source_view#buffer#paste_clipboard clipboard;
+          (MatitaScript.instance ())#clean_dirty_lock));
+      ignore(self#main#deleteMenuItem#connect#activate
+        ~callback:(fun () -> ignore (source_view#buffer#delete_selection ())));
       ignore(self#main#findReplMenuItem#connect#activate
         ~callback:show_find_Repl);
       ignore (findRepl#findEntry#connect#activate ~callback:find_forward);