src/Tools/jEdit/src/jedit_lib.scala

--- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Sep 18 15:09:15 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Sep 18 15:50:59 2013 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle, Dimension}
+import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension}
 import java.awt.event.{KeyEvent, KeyListener}
 import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
 
@@ -92,30 +92,6 @@
   }
 
 
-  /* GUI components */
-
-  def get_parent(component: Component): Option[Container] =
-    component.getParent match {
-      case null => None
-      case parent => Some(parent)
-    }
-
-  def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
-    private var next_elem = get_parent(component)
-    def hasNext(): Boolean = next_elem.isDefined
-    def next(): Container =
-      next_elem match {
-        case Some(parent) =>
-          next_elem = get_parent(parent)
-          parent
-        case None => Iterator.empty.next()
-      }
-  }
-
-  def parent_window(component: Component): Option[Window] =
-    ancestors(component).collectFirst({ case x: Window => x })
-
-
   /* basic tooltips, with multi-line support */
 
   def wrap_tooltip(text: String): String =