1. select_all added to the Edit menu; no shortcut for it (since the standard

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 7eaf239e1680cade11e6a10d27000182a0ac8013..216dc9d5b79d2cbef8536142a6332ffce2f20db8 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -353,6 +353,11 @@ class gui () =
           (MatitaScript.instance ())#clean_dirty_lock));
       ignore(self#main#deleteMenuItem#connect#activate
         ~callback:(fun () -> ignore (source_view#buffer#delete_selection ())));
+      ignore(self#main#selectAllMenuItem#connect#activate
+        ~callback:(fun () ->
+          source_buffer#move_mark `INSERT (source_buffer#get_iter `START);
+          source_buffer#move_mark `SEL_BOUND (source_buffer#get_iter `END)
+          ));
       ignore(self#main#findReplMenuItem#connect#activate
         ~callback:show_find_Repl);
       ignore (findRepl#findEntry#connect#activate ~callback:find_forward);