--- 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 })
}
--- 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))
}
}
--- 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()
}
--- 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 =
--- 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)
}