# HG changeset patch
# User wenzelm
# Date 1376389185 -7200
# Node ID 0ef4699b2502c46ccdd94a39b47a880c11b1539b
# Parent  50d06647cf24d8d83aabfe19e2ccb6b0d3ac522a
support somewhat standard "select all" by default;

diff -r 50d06647cf24 -r 0ef4699b2502 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Aug 13 11:57:42 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Aug 13 12:19:45 2013 +0200
@@ -170,6 +170,10 @@
         if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
           Registers.copy(text_area, '$')
           evt.consume
+        case KeyEvent.VK_A
+        if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
+          text_area.selectAll
+          evt.consume
         case _ =>
       }
       if (propagate_keys && !evt.isConsumed)