# HG changeset patch
# User wenzelm
# Date 1373213086 -7200
# Node ID a1a8248a4677f076fe74a5ed147bcc9548d7dc9b
# Parent  0ddcfc0d05d4ad7ca1750b37e00fd9034109b5cb
some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;

diff -r 0ddcfc0d05d4 -r a1a8248a4677 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Sun Jul 07 17:52:13 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Sun Jul 07 18:04:46 2013 +0200
@@ -152,7 +152,8 @@
   private val key_listener = new KeyAdapter {
     override def keyTyped(evt: KeyEvent)
     {
-      if (evt.getKeyChar == 27) Pretty_Tooltip.dismiss_all()
+      if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all())
+        evt.consume
     }
   }
 
diff -r 0ddcfc0d05d4 -r a1a8248a4677 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Jul 07 17:52:13 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Jul 07 18:04:46 2013 +0200
@@ -178,7 +178,8 @@
 
     override def keyTyped(evt: KeyEvent)
     {
-      if (evt.getKeyChar == 27) Pretty_Tooltip.dismiss_all()
+      if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all())
+        evt.consume
 
       if (propagate_keys && !evt.isConsumed)
         view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false)
diff -r 0ddcfc0d05d4 -r a1a8248a4677 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Jul 07 17:52:13 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Jul 07 18:04:46 2013 +0200
@@ -117,12 +117,14 @@
     }
   }
 
-  def dismiss_all()
-  {
-    deactivate()
-    stack.foreach(_.hide_popup)
-    stack = Nil
-  }
+  def dismissed_all(): Boolean =
+    if (stack.isEmpty) false
+    else {
+      deactivate()
+      stack.foreach(_.hide_popup)
+      stack = Nil
+      true
+    }
 
 
   /* auxiliary geometry measurement */
diff -r 0ddcfc0d05d4 -r a1a8248a4677 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Jul 07 17:52:13 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Jul 07 18:04:46 2013 +0200
@@ -156,7 +156,7 @@
       robust_body(()) {
         hyperlink_area.info match {
           case Some(Text.Info(_, link)) =>
-            Pretty_Tooltip.dismiss_all()
+            Pretty_Tooltip.dismissed_all()
             link.follow(view)
           case None =>
         }