# HG changeset patch
# User wenzelm
# Date 1377601651 -7200
# Node ID 68cc55ceb7f6f013b5a275f30cdb705fcbe19504
# Parent  9cf8e2263ca74046146ed81bde15ec6e62d0e513
more standard key handling according to jEdit (with workaround);
clarified handling of ESCAPE (again): dismiss without second interpretation as select-none;

diff -r 9cf8e2263ca7 -r 68cc55ceb7f6 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 12:35:32 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Aug 27 13:07:31 2013 +0200
@@ -151,10 +151,9 @@
 
   private val key_listener =
     JEdit_Lib.key_listener(
-      workaround = false,
-      key_typed = (evt: KeyEvent) =>
+      key_pressed = (evt: KeyEvent) =>
         {
-          if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all())
+          if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Pretty_Tooltip.dismissed_all())
             evt.consume
         }
     )
diff -r 9cf8e2263ca7 -r 68cc55ceb7f6 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Aug 27 12:35:32 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Aug 27 13:07:31 2013 +0200
@@ -163,7 +163,6 @@
   /* key handling */
 
   addKeyListener(JEdit_Lib.key_listener(
-    workaround = false,
     key_pressed = (evt: KeyEvent) =>
       {
         evt.getKeyCode match {
@@ -171,10 +170,15 @@
           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 KeyEvent.VK_ESCAPE =>
+            if (Pretty_Tooltip.dismissed_all()) evt.consume
+
           case _ =>
         }
         if (propagate_keys && !evt.isConsumed)
@@ -182,8 +186,6 @@
       },
     key_typed = (evt: KeyEvent) =>
       {
-        if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all())
-          evt.consume
         if (propagate_keys && !evt.isConsumed)
           view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false)
       }