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

[helm.git] / helm / matita / matitaGui.ml

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);