# HG changeset patch
# User wenzelm
# Date 1379512259 -7200
# Node ID ea51046be71b0c3ef42358cfb3d0b31a38c55d1b
# Parent  8ce7795256e157e9968e45a060455861d3924b9b
tuned signature;

diff -r 8ce7795256e1 -r ea51046be71b src/Pure/System/gui.scala
--- a/src/Pure/System/gui.scala	Wed Sep 18 15:09:15 2013 +0200
+++ b/src/Pure/System/gui.scala	Wed Sep 18 15:50:59 2013 +0200
@@ -1,13 +1,13 @@
 /*  Title:      Pure/System/gui.scala
     Author:     Makarius
 
-Elementary GUI tools.
+Basic GUI tools (for AWT/Swing).
 */
 
 package isabelle
 
 
-import java.awt.{Image, Component, Toolkit}
+import java.awt.{Image, Component, Container, Toolkit, Window}
 import javax.swing.{ImageIcon, JOptionPane, UIManager}
 
 import scala.swing.{ComboBox, TextArea, ScrollPane}
@@ -117,5 +117,29 @@
     new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif"))
 
   def isabelle_image(): Image = isabelle_icon().getImage
+
+
+  /* component hierachy */
+
+  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 })
 }
 
diff -r 8ce7795256e1 -r ea51046be71b src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Wed Sep 18 15:09:15 2013 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Wed Sep 18 15:50:59 2013 +0200
@@ -78,11 +78,11 @@
 
   override def init()
   {
-    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
   }
 
   override def exit()
   {
-    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
   }
 }
diff -r 8ce7795256e1 -r ea51046be71b src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Wed Sep 18 15:09:15 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Wed Sep 18 15:50:59 2013 +0200
@@ -113,14 +113,14 @@
 
   override def init()
   {
-    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
     PIDE.session.global_options += main_actor
     handle_resize()
   }
 
   override def exit()
   {
-    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
     PIDE.session.global_options -= main_actor
     delay_resize.revoke()
   }
diff -r 8ce7795256e1 -r ea51046be71b 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 =
diff -r 8ce7795256e1 -r ea51046be71b src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Sep 18 15:09:15 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Sep 18 15:50:59 2013 +0200
@@ -50,7 +50,7 @@
       case top :: _ if top.results == results && top.info == info => top
       case _ =>
         val (old, rest) =
-          JEdit_Lib.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
+          GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
             case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
             case None => (stack, Nil)
           }