--- a/src/Tools/jEdit/src/jedit_lib.scala Mon Dec 31 20:30:03 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Dec 31 21:01:00 2012 +0100
@@ -9,7 +9,7 @@
import isabelle._
-import java.awt.{Component, Container, Frame, Window, GraphicsEnvironment, Point, Rectangle}
+import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
import scala.annotation.tailrec
@@ -56,9 +56,6 @@
def parent_window(component: Component): Option[Window] =
ancestors(component).find(_.isInstanceOf[Window]).map(_.asInstanceOf[Window])
- def parent_frame(component: Component): Option[Frame] =
- ancestors(component).find(_.isInstanceOf[Frame]).map(_.asInstanceOf[Frame])
-
/* basic tooltips, with multi-line support */