# HG changeset patch
# User wenzelm
# Date 1372520367 -7200
# Node ID bb516d01d2595b36cb06c4165792adbaa32b7ea5
# Parent  0a1db0d02628828bfd3d108002e6fead2c68e980
more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;

diff -r 0a1db0d02628 -r bb516d01d259 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Sat Jun 29 16:53:19 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Sat Jun 29 17:39:27 2013 +0200
@@ -17,13 +17,14 @@
 import java.lang.System
 import java.text.BreakIterator
 import java.awt.{Color, Graphics2D, Point}
+import java.awt.event.{KeyEvent, KeyAdapter}
 import javax.swing.event.{CaretListener, CaretEvent}
 
 import org.gjt.sp.jedit.{jEdit, Debug}
 import org.gjt.sp.jedit.gui.RolloverButton
 import org.gjt.sp.jedit.options.GutterOptionPane
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
-import org.gjt.sp.jedit.syntax.{SyntaxStyle}
+import org.gjt.sp.jedit.syntax.SyntaxStyle
 
 
 object Document_View
@@ -146,6 +147,16 @@
   }
 
 
+  /* key listener */
+
+  private val key_listener = new KeyAdapter {
+    override def keyTyped(evt: KeyEvent)
+    {
+      if (evt.getKeyChar == 27) Pretty_Tooltip.dismiss_all()
+    }
+  }
+
+
   /* caret handling */
 
   private val delay_caret_update =
@@ -227,6 +238,7 @@
     painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
     rich_text_area.activate()
     text_area.getGutter.addExtension(gutter_painter)
+    text_area.addKeyListener(key_listener)
     text_area.addCaretListener(caret_listener)
     text_area.addLeftOfScrollBar(overview)
     session.raw_edits += main_actor
@@ -239,8 +251,9 @@
 
     session.raw_edits -= main_actor
     session.commands_changed -= main_actor
+    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
     text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
-    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
+    text_area.removeKeyListener(key_listener)
     text_area.getGutter.removeExtension(gutter_painter)
     rich_text_area.deactivate()
     painter.removeExtension(update_perspective)
diff -r 0a1db0d02628 -r bb516d01d259 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)
     }