refer to parent frame -- relevant for floating dockables in particular;
authorwenzelm
Fri Oct 05 13:48:22 2012 +0200 (2012-10-05)
changeset 4971021d88a631fcc
parent 49709 3062937b45b3
child 49711 e5aaae7eadc9
refer to parent frame -- relevant for floating dockables in particular;
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/pretty_tooltip.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 05 12:11:23 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 05 13:48:22 2012 +0200
     1.3 @@ -9,6 +9,9 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 +import java.awt.{Component, Container, Frame}
     1.8 +
     1.9 +import scala.annotation.tailrec
    1.10  
    1.11  import org.gjt.sp.jedit.{jEdit, Buffer, View}
    1.12  import org.gjt.sp.jedit.buffer.JEditBuffer
    1.13 @@ -17,6 +20,20 @@
    1.14  
    1.15  object JEdit_Lib
    1.16  {
    1.17 +  /* frames */
    1.18 +
    1.19 +  def parent_frame(component: Component): Option[Frame] =
    1.20 +  {
    1.21 +    @tailrec def find(c: Container): Option[Frame] =
    1.22 +      c match {
    1.23 +        case null => None
    1.24 +        case frame: Frame => Some(frame)
    1.25 +        case _ => find(c.getParent)
    1.26 +      }
    1.27 +    find(component.getParent)
    1.28 +  }
    1.29 +
    1.30 +
    1.31    /* buffers */
    1.32  
    1.33    def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
     2.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 12:11:23 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 05 13:48:22 2012 +0200
     2.3 @@ -22,7 +22,8 @@
     2.4    view: View,
     2.5    text_area: TextArea,
     2.6    rendering: Isabelle_Rendering,
     2.7 -  mouse_x: Int, mouse_y: Int, body: XML.Body) extends JWindow(view)
     2.8 +  mouse_x: Int, mouse_y: Int, body: XML.Body)
     2.9 +  extends JWindow(JEdit_Lib.parent_frame(text_area) getOrElse view)
    2.10  {
    2.11    window =>
    2.12