tuned signature;
authorwenzelm
Mon Dec 31 21:01:00 2012 +0100 (2012-12-31)
changeset 506580464c2007a25
parent 50657 57abb2a814ab
child 50659 0f88591478e6
tuned signature;
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 31 20:30:03 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 31 21:01:00 2012 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import java.awt.{Component, Container, Frame, Window, GraphicsEnvironment, Point, Rectangle}
     1.8 +import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
     1.9  
    1.10  import scala.annotation.tailrec
    1.11  
    1.12 @@ -56,9 +56,6 @@
    1.13    def parent_window(component: Component): Option[Window] =
    1.14      ancestors(component).find(_.isInstanceOf[Window]).map(_.asInstanceOf[Window])
    1.15  
    1.16 -  def parent_frame(component: Component): Option[Frame] =
    1.17 -    ancestors(component).find(_.isInstanceOf[Frame]).map(_.asInstanceOf[Frame])
    1.18 -
    1.19  
    1.20    /* basic tooltips, with multi-line support */
    1.21