1 /* Title: Pure/GUI/gui.scala
5 Basic GUI tools (for AWT/Swing).
11 import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException}
12 import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
13 import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
14 import java.awt.geom.AffineTransform
15 import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow,
18 import scala.collection.convert.WrapAsJava
19 import scala.swing.{ComboBox, TextArea, ScrollPane}
20 import scala.swing.event.SelectionChanged
25 /* Swing look-and-feel */
27 def get_laf(): String =
29 if (Platform.is_windows || Platform.is_macos)
30 UIManager.getSystemLookAndFeelClassName()
32 UIManager.getInstalledLookAndFeels().find(_.getName == "Nimbus").map(_.getClassName)
33 .getOrElse(UIManager.getCrossPlatformLookAndFeelClassName())
36 def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
38 def is_macos_laf(): Boolean =
40 UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName
43 /* plain focus traversal, notably for text fields */
45 def plain_focus_traversal(component: Component)
47 val dummy_button = new JButton
48 def apply(id: Int): Unit =
49 component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id))
50 apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS)
51 apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS)
55 /* X11 window manager */
57 def window_manager(): Option[String] =
59 if (Platform.is_windows || Platform.is_macos) None
62 val XWM = Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader)
63 val getWM = XWM.getDeclaredMethod("getWM")
64 getWM.setAccessible(true)
65 getWM.invoke(null) match {
67 case wm => Some(wm.toString)
71 case _: ClassNotFoundException => None
72 case _: NoSuchMethodException => None
79 def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
82 val text = new TextArea(txt)
83 if (width > 0) text.columns = width
84 if (height > 0 && split_lines(txt).length > height) text.rows = height
85 text.editable = editable
89 private def simple_dialog(kind: Int, default_title: String,
90 parent: Component, title: String, message: Seq[Any])
93 val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
94 JOptionPane.showMessageDialog(parent,
95 java_message.toArray.asInstanceOf[Array[AnyRef]],
96 if (title == null) default_title else title, kind)
100 def dialog(parent: Component, title: String, message: Any*) =
101 simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
103 def warning_dialog(parent: Component, title: String, message: Any*) =
104 simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
106 def error_dialog(parent: Component, title: String, message: Any*) =
107 simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
109 def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
111 val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
112 JOptionPane.showConfirmDialog(parent,
113 java_message.toArray.asInstanceOf[Array[AnyRef]], title,
114 option_type, JOptionPane.QUESTION_MESSAGE)
120 class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
121 List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
123 val Factor = "([0-9]+)%?".r
124 def parse(text: String): Int =
127 val i = Integer.parseInt(s)
128 if (10 <= i && i < 1000) i else 100
132 def print(i: Int): String = i.toString + "%"
134 def set_item(i: Int) {
135 peer.getEditor match {
137 case editor => editor.setItem(print(i))
141 makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
142 peer.getEditor.getEditorComponent match {
143 case text: JTextField => text.setColumns(4)
148 case SelectionChanged(_) => apply_factor(parse(selection.item))
155 /* tooltip with multi-line support */
157 def tooltip_lines(text: String): String =
158 if (text == null || text == "") null
159 else "<html>" + HTML.encode(text) + "</html>"
162 /* screen resolution */
164 def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72
165 def resolution_scale(i: Int): Int = (i.toDouble * resolution_scale()).round.toInt
170 def isabelle_icon(): ImageIcon =
171 new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle_transparent-32.gif"))
173 def isabelle_icons(): List[ImageIcon] =
174 for (icon <- List("isabelle/isabelle_transparent-32.gif", "isabelle/isabelle_transparent.gif"))
175 yield new ImageIcon(getClass.getClassLoader.getResource(icon))
177 def isabelle_image(): Image = isabelle_icon().getImage
179 def isabelle_images(): java.util.List[Image] =
180 WrapAsJava.seqAsJavaList(isabelle_icons.map(_.getImage))
183 /* component hierachy */
185 def get_parent(component: Component): Option[Container] =
186 component.getParent match {
188 case parent => Some(parent)
191 def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
192 private var next_elem = get_parent(component)
193 def hasNext(): Boolean = next_elem.isDefined
194 def next(): Container =
197 next_elem = get_parent(parent)
199 case None => Iterator.empty.next()
203 def parent_window(component: Component): Option[Window] =
204 ancestors(component).collectFirst({ case x: Window => x })
206 def layered_pane(component: Component): Option[JLayeredPane] =
207 parent_window(component) match {
208 case Some(window: JWindow) => Some(window.getLayeredPane)
209 case Some(frame: JFrame) => Some(frame.getLayeredPane)
214 /* font operations */
216 def font_metrics(font: Font): LineMetrics =
217 font.getLineMetrics("", new FontRenderContext(null, false, false))
219 def imitate_font(family: String, font: Font, scale: Double = 1.0): Font =
221 val font1 = new Font(family, font.getStyle, font.getSize)
222 val size = scale * (font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
223 font1.deriveFont(size.round.toInt)
226 def transform_font(font: Font, transform: AffineTransform): Font =
228 import scala.collection.JavaConversions._
229 font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))