The edit menu items (copy/cut/delete/paste) are now sensitive to the

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index f83e01913d7fb1c26281e4ef5a60492e39301b67..7eaf239e1680cade11e6a10d27000182a0ac8013 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -331,6 +331,18 @@ class gui () =
       let clipboard =
        let atom = Gdk.Atom.clipboard in
         GData.clipboard atom in
+      ignore(self#main#editMenu#connect#activate
+        ~callback:
+          (fun () ->
+            let something_selected =
+              (source_buffer#get_iter_at_mark `INSERT)#compare
+              (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
+            in
+             self#main#cutMenuItem#misc#set_sensitive something_selected;
+             self#main#copyMenuItem#misc#set_sensitive something_selected;
+             self#main#deleteMenuItem#misc#set_sensitive something_selected;
+             self#main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None)
+          ));
       ignore(self#main#cutMenuItem#connect#activate
         ~callback:(fun () -> source_view#buffer#cut_clipboard clipboard));
       ignore(self#main#copyMenuItem#connect#activate