# HG changeset patch
# User wenzelm
# Date 1349440376 -7200
# Node ID a1bd8fe5131bd47dd89401fa1f0629c85c99d4d5
# Parent  e5aaae7eadc993cd160b5bdb5af155de18948af9
further support for nested tooltips;

diff -r e5aaae7eadc9 -r a1bd8fe5131b src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 05 13:57:48 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 05 14:32:56 2012 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.awt.{Component, Container, Frame}
+import java.awt.{Component, Container, Frame, Window}
 
 import scala.annotation.tailrec
 
@@ -20,18 +20,31 @@
 
 object JEdit_Lib
 {
-  /* frames */
+  /* GUI components */
+
+  def get_parent(component: Component): Option[Container] =
+    component.getParent match {
+      case null => None
+      case parent => Some(parent)
+    }
+
+  def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
+    private var next_elem = get_parent(component)
+    def hasNext(): Boolean = next_elem.isDefined
+    def next(): Container =
+      next_elem match {
+        case Some(parent) =>
+          next_elem = get_parent(parent)
+          parent
+        case None => Iterator.empty.next()
+      }
+  }
+
+  def parent_window(component: Component): Option[Window] =
+    ancestors(component).find(_.isInstanceOf[Window]).map(_.asInstanceOf[Window])
 
   def parent_frame(component: Component): Option[Frame] =
-  {
-    @tailrec def find(c: Container): Option[Frame] =
-      c match {
-        case null => None
-        case frame: Frame => Some(frame)
-        case _ => find(c.getParent)
-      }
-    find(component.getParent)
-  }
+    ancestors(component).find(_.isInstanceOf[Frame]).map(_.asInstanceOf[Frame])
 
 
   /* buffers */
diff -r e5aaae7eadc9 -r a1bd8fe5131b src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 13:57:48 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 14:32:56 2012 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.awt.{Toolkit, Color, Point, BorderLayout}
+import java.awt.{Toolkit, Color, Point, BorderLayout, Window}
 import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
 import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, KeyStroke}
 import javax.swing.border.LineBorder
@@ -23,19 +23,28 @@
   text_area: TextArea,
   rendering: Isabelle_Rendering,
   mouse_x: Int, mouse_y: Int, body: XML.Body)
-  extends JWindow(JEdit_Lib.parent_frame(text_area) getOrElse view)
+  extends JWindow(JEdit_Lib.parent_window(text_area) getOrElse view)
 {
   window =>
 
   window.addWindowFocusListener(new WindowAdapter {
-    override def windowLostFocus(e: WindowEvent) { window.dispose() }
+    override def windowLostFocus(e: WindowEvent) {
+      if (!Window.getWindows.exists(w =>
+            w.isDisplayable && JEdit_Lib.ancestors(w).exists(_ == window)))
+        window.dispose()
+    }
   })
 
   window.setContentPane(new JPanel(new BorderLayout) {
     private val action_listener = new ActionListener {
       def actionPerformed(e: ActionEvent) {
         e.getActionCommand match {
-          case "close" => window.dispose()
+          case "close" =>
+            window.dispose()
+            JEdit_Lib.ancestors(window) foreach {
+              case c: Pretty_Tooltip => c.dispose
+              case _ =>
+            }
           case _ =>
         }
       }