# HG changeset patch
# User wenzelm
# Date 1356984060 -3600
# Node ID 0464c2007a255319552dd869186c1a679b1cb4ec
# Parent  57abb2a814ab130ce8d1c6fe3f6bdc9be90dec31
tuned signature;

diff -r 57abb2a814ab -r 0464c2007a25 src/Tools/jEdit/src/jedit_lib.scala
--- 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 */