1.1 --- a/src/Pure/System/gui.scala	Wed Sep 18 15:09:15 2013 +0200
     1.2 +++ b/src/Pure/System/gui.scala	Wed Sep 18 15:50:59 2013 +0200
     1.3 @@ -1,13 +1,13 @@
     1.4  /*  Title:      Pure/System/gui.scala
     1.5      Author:     Makarius
     1.6  
     1.7 -Elementary GUI tools.
     1.8 +Basic GUI tools (for AWT/Swing).
     1.9  */
    1.10  
    1.11  package isabelle
    1.12  
    1.13  
    1.14 -import java.awt.{Image, Component, Toolkit}
    1.15 +import java.awt.{Image, Component, Container, Toolkit, Window}
    1.16  import javax.swing.{ImageIcon, JOptionPane, UIManager}
    1.17  
    1.18  import scala.swing.{ComboBox, TextArea, ScrollPane}
    1.19 @@ -117,5 +117,29 @@
    1.20      new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif"))
    1.21  
    1.22    def isabelle_image(): Image = isabelle_icon().getImage
    1.23 +
    1.24 +
    1.25 +  /* component hierachy */
    1.26 +
    1.27 +  def get_parent(component: Component): Option[Container] =
    1.28 +    component.getParent match {
    1.29 +      case null => None
    1.30 +      case parent => Some(parent)
    1.31 +    }
    1.32 +
    1.33 +  def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
    1.34 +    private var next_elem = get_parent(component)
    1.35 +    def hasNext(): Boolean = next_elem.isDefined
    1.36 +    def next(): Container =
    1.37 +      next_elem match {
    1.38 +        case Some(parent) =>
    1.39 +          next_elem = get_parent(parent)
    1.40 +          parent
    1.41 +        case None => Iterator.empty.next()
    1.42 +      }
    1.43 +  }
    1.44 +
    1.45 +  def parent_window(component: Component): Option[Window] =
    1.46 +    ancestors(component).collectFirst({ case x: Window => x })
    1.47  }
    1.48  

     2.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Wed Sep 18 15:09:15 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Wed Sep 18 15:50:59 2013 +0200
     2.3 @@ -78,11 +78,11 @@
     2.4  
     2.5    override def init()
     2.6    {
     2.7 -    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
     2.8 +    GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
     2.9    }
    2.10  
    2.11    override def exit()
    2.12    {
    2.13 -    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
    2.14 +    GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
    2.15    }
    2.16  }

     3.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Wed Sep 18 15:09:15 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Wed Sep 18 15:50:59 2013 +0200
     3.3 @@ -113,14 +113,14 @@
     3.4  
     3.5    override def init()
     3.6    {
     3.7 -    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
     3.8 +    GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
     3.9      PIDE.session.global_options += main_actor
    3.10      handle_resize()
    3.11    }
    3.12  
    3.13    override def exit()
    3.14    {
    3.15 -    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
    3.16 +    GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
    3.17      PIDE.session.global_options -= main_actor
    3.18      delay_resize.revoke()
    3.19    }

     4.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Sep 18 15:09:15 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Sep 18 15:50:59 2013 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  
     4.5  import isabelle._
     4.6  
     4.7 -import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle, Dimension}
     4.8 +import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension}
     4.9  import java.awt.event.{KeyEvent, KeyListener}
    4.10  import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
    4.11  
    4.12 @@ -92,30 +92,6 @@
    4.13    }
    4.14  
    4.15  
    4.16 -  /* GUI components */
    4.17 -
    4.18 -  def get_parent(component: Component): Option[Container] =
    4.19 -    component.getParent match {
    4.20 -      case null => None
    4.21 -      case parent => Some(parent)
    4.22 -    }
    4.23 -
    4.24 -  def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
    4.25 -    private var next_elem = get_parent(component)
    4.26 -    def hasNext(): Boolean = next_elem.isDefined
    4.27 -    def next(): Container =
    4.28 -      next_elem match {
    4.29 -        case Some(parent) =>
    4.30 -          next_elem = get_parent(parent)
    4.31 -          parent
    4.32 -        case None => Iterator.empty.next()
    4.33 -      }
    4.34 -  }
    4.35 -
    4.36 -  def parent_window(component: Component): Option[Window] =
    4.37 -    ancestors(component).collectFirst({ case x: Window => x })
    4.38 -
    4.39 -
    4.40    /* basic tooltips, with multi-line support */
    4.41  
    4.42    def wrap_tooltip(text: String): String =

     5.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Sep 18 15:09:15 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Sep 18 15:50:59 2013 +0200
     5.3 @@ -50,7 +50,7 @@
     5.4        case top :: _ if top.results == results && top.info == info => top
     5.5        case _ =>
     5.6          val (old, rest) =
     5.7 -          JEdit_Lib.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
     5.8 +          GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
     5.9              case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
    5.10              case None => (stack, Nil)
    5.11            }