src/Tools/jEdit/src/pretty_text_area.scala

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Jun 29 16:53:19 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Jun 29 17:39:27 2013 +0200
@@ -170,9 +170,6 @@
         if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
           Registers.copy(text_area, '$')
           evt.consume
-        case KeyEvent.VK_ESCAPE =>
-          Pretty_Tooltip.dismiss_all()
-          evt.consume
         case _ =>
       }
       if (propagate_keys && !evt.isConsumed)
@@ -181,6 +178,8 @@
 
     override def keyTyped(evt: KeyEvent)
     {
+      if (evt.getKeyChar == 27) Pretty_Tooltip.dismiss_all()
+
       if (propagate_keys && !evt.isConsumed)
         view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false)
     }