--- 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 =
--- 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 =>