equal
deleted
inserted
replaced
1 /* Title: Pure/System/gui.scala |
1 /* Title: Pure/System/gui.scala |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Elementary GUI tools. |
4 Basic GUI tools (for AWT/Swing). |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 import java.awt.{Image, Component, Toolkit} |
10 import java.awt.{Image, Component, Container, Toolkit, Window} |
11 import javax.swing.{ImageIcon, JOptionPane, UIManager} |
11 import javax.swing.{ImageIcon, JOptionPane, UIManager} |
12 |
12 |
13 import scala.swing.{ComboBox, TextArea, ScrollPane} |
13 import scala.swing.{ComboBox, TextArea, ScrollPane} |
14 import scala.swing.event.SelectionChanged |
14 import scala.swing.event.SelectionChanged |
15 |
15 |
115 |
115 |
116 def isabelle_icon(): ImageIcon = |
116 def isabelle_icon(): ImageIcon = |
117 new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif")) |
117 new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif")) |
118 |
118 |
119 def isabelle_image(): Image = isabelle_icon().getImage |
119 def isabelle_image(): Image = isabelle_icon().getImage |
|
120 |
|
121 |
|
122 /* component hierachy */ |
|
123 |
|
124 def get_parent(component: Component): Option[Container] = |
|
125 component.getParent match { |
|
126 case null => None |
|
127 case parent => Some(parent) |
|
128 } |
|
129 |
|
130 def ancestors(component: Component): Iterator[Container] = new Iterator[Container] { |
|
131 private var next_elem = get_parent(component) |
|
132 def hasNext(): Boolean = next_elem.isDefined |
|
133 def next(): Container = |
|
134 next_elem match { |
|
135 case Some(parent) => |
|
136 next_elem = get_parent(parent) |
|
137 parent |
|
138 case None => Iterator.empty.next() |
|
139 } |
|
140 } |
|
141 |
|
142 def parent_window(component: Component): Option[Window] = |
|
143 ancestors(component).collectFirst({ case x: Window => x }) |
120 } |
144 } |
121 |
145 |