# HG changeset patch
# User wenzelm
# Date 1396291530 -7200
# Node ID bfd13102eb541fda5a9fc36b291a78aab07719f2
# Parent  af8cb60b55eb12acd85ac35df560e9d9ff7050ae
observe focus change for all tooltips, e.g. relevant for focus change to unrelated components;

diff -r af8cb60b55eb -r bfd13102eb54 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Mar 31 20:07:59 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Mar 31 20:45:30 2014 +0200
@@ -110,6 +110,22 @@
 
   /* dismiss */
 
+  private lazy val focus_delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
+  {
+    dismiss_unfocused()
+  }
+
+  def dismiss_unfocused()
+  {
+    stack.span(tip => !tip.pretty_text_area.isFocusOwner) match {
+      case (Nil, _) =>
+      case (unfocused, rest) =>
+        deactivate()
+        unfocused.foreach(_.hide_popup)
+        stack = rest
+    }
+  }
+
   def dismiss(tip: Pretty_Tooltip)
   {
     deactivate()
@@ -189,13 +205,12 @@
     override def focusGained(e: FocusEvent)
     {
       tip_border(true)
+      Pretty_Tooltip.focus_delay.invoke()
     }
     override def focusLost(e: FocusEvent)
     {
-      Pretty_Tooltip.hierarchy(tip) match {
-        case Some((Nil, _)) => Pretty_Tooltip.dismiss(tip)
-        case _ => tip_border(false)
-      }
+      tip_border(false)
+      Pretty_Tooltip.focus_delay.invoke()
     }
   })