# HG changeset patch
# User wenzelm
# Date 1349437702 -7200
# Node ID 21d88a631fcce7cde59806de20e6e84dccfddd68
# Parent  3062937b45b3afbabf91ce29fdc84a0ebee4fa3b
refer to parent frame -- relevant for floating dockables in particular;

diff -r 3062937b45b3 -r 21d88a631fcc src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 05 12:11:23 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 05 13:48:22 2012 +0200
@@ -9,6 +9,9 @@
 
 import isabelle._
 
+import java.awt.{Component, Container, Frame}
+
+import scala.annotation.tailrec
 
 import org.gjt.sp.jedit.{jEdit, Buffer, View}
 import org.gjt.sp.jedit.buffer.JEditBuffer
@@ -17,6 +20,20 @@
 
 object JEdit_Lib
 {
+  /* frames */
+
+  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)
+  }
+
+
   /* buffers */
 
   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
diff -r 3062937b45b3 -r 21d88a631fcc src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 12:11:23 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 13:48:22 2012 +0200
@@ -22,7 +22,8 @@
   view: View,
   text_area: TextArea,
   rendering: Isabelle_Rendering,
-  mouse_x: Int, mouse_y: Int, body: XML.Body) extends JWindow(view)
+  mouse_x: Int, mouse_y: Int, body: XML.Body)
+  extends JWindow(JEdit_Lib.parent_frame(text_area) getOrElse view)
 {
   window =>