support somewhat standard "select all" by default;

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