1/* Title: Pure/GUI/gui.scala 2 Author: Makarius 3 4Basic GUI tools (for AWT/Swing). 5*/ 6 7package isabelle 8 9import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException} 10import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager} 11import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics} 12import java.awt.geom.AffineTransform 13import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog, 14 JButton, JTextField, JLabel} 15 16 17import scala.collection.JavaConverters 18import scala.swing.{ComboBox, TextArea, ScrollPane} 19import scala.swing.event.SelectionChanged 20 21 22object GUI 23{ 24 /* Swing look-and-feel */ 25 26 def find_laf(name: String): Option[String] = 27 UIManager.getInstalledLookAndFeels(). 28 find(c => c.getName == name || c.getClassName == name). 29 map(_.getClassName) 30 31 def get_laf(): String = 32 find_laf(System.getProperty("isabelle.laf")) getOrElse { 33 if (Platform.is_windows || Platform.is_macos) 34 UIManager.getSystemLookAndFeelClassName() 35 else 36 UIManager.getCrossPlatformLookAndFeelClassName() 37 } 38 39 def init_laf(): Unit = UIManager.setLookAndFeel(get_laf()) 40 41 def is_macos_laf(): Boolean = 42 Platform.is_macos && 43 UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName 44 45 def is_windows_laf(): Boolean = 46 Platform.is_windows && 47 UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName 48 49 50 /* plain focus traversal, notably for text fields */ 51 52 def plain_focus_traversal(component: Component) 53 { 54 val dummy_button = new JButton 55 def apply(id: Int): Unit = 56 component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id)) 57 apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS) 58 apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS) 59 } 60 61 62 /* simple dialogs */ 63 64 def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false) 65 : ScrollPane = 66 { 67 val txt = Output.clean_yxml(raw_txt) 68 val text = new TextArea(txt) 69 if (width > 0) text.columns = width 70 if (height > 0 && split_lines(txt).length > height) text.rows = height 71 text.editable = editable 72 new ScrollPane(text) 73 } 74 75 private def simple_dialog(kind: Int, default_title: String, 76 parent: Component, title: String, message: Iterable[Any]) 77 { 78 GUI_Thread.now { 79 val java_message = 80 message.iterator.map({ case x: scala.swing.Component => x.peer case x => x }). 81 toArray.asInstanceOf[Array[AnyRef]] 82 JOptionPane.showMessageDialog(parent, java_message, 83 if (title == null) default_title else title, kind) 84 } 85 } 86 87 def dialog(parent: Component, title: String, message: Any*): Unit = 88 simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message) 89 90 def warning_dialog(parent: Component, title: String, message: Any*): Unit = 91 simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message) 92 93 def error_dialog(parent: Component, title: String, message: Any*): Unit = 94 simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message) 95 96 def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int = 97 GUI_Thread.now { 98 val java_message = message map { case x: scala.swing.Component => x.peer case x => x } 99 JOptionPane.showConfirmDialog(parent, 100 java_message.toArray.asInstanceOf[Array[AnyRef]], title, 101 option_type, JOptionPane.QUESTION_MESSAGE) 102 } 103 104 105 /* zoom box */ 106 107 private val Zoom_Factor = "([0-9]+)%?".r 108 109 abstract class Zoom_Box extends ComboBox[String]( 110 List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) 111 { 112 def changed: Unit 113 def factor: Int = parse(selection.item) 114 115 private def parse(text: String): Int = 116 text match { 117 case Zoom_Factor(s) => 118 val i = Integer.parseInt(s) 119 if (10 <= i && i < 1000) i else 100 120 case _ => 100 121 } 122 123 private def print(i: Int): String = i.toString + "%" 124 125 def set_item(i: Int) { 126 peer.getEditor match { 127 case null => 128 case editor => editor.setItem(print(i)) 129 } 130 } 131 132 makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x)) 133 peer.getEditor.getEditorComponent match { 134 case text: JTextField => text.setColumns(4) 135 case _ => 136 } 137 138 selection.index = 3 139 140 listenTo(selection) 141 reactions += { case SelectionChanged(_) => changed } 142 } 143 144 145 /* tooltip with multi-line support */ 146 147 def tooltip_lines(text: String): String = 148 if (text == null || text == "") null 149 else "<html>" + HTML.output(text) + "</html>" 150 151 152 /* icon */ 153 154 def isabelle_icon(): ImageIcon = 155 new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle_transparent-32.gif")) 156 157 def isabelle_icons(): List[ImageIcon] = 158 for (icon <- List("isabelle/isabelle_transparent-32.gif", "isabelle/isabelle_transparent.gif")) 159 yield new ImageIcon(getClass.getClassLoader.getResource(icon)) 160 161 def isabelle_image(): Image = isabelle_icon().getImage 162 163 164 /* component hierachy */ 165 166 def get_parent(component: Component): Option[Container] = 167 component.getParent match { 168 case null => None 169 case parent => Some(parent) 170 } 171 172 def ancestors(component: Component): Iterator[Container] = new Iterator[Container] { 173 private var next_elem = get_parent(component) 174 def hasNext(): Boolean = next_elem.isDefined 175 def next(): Container = 176 next_elem match { 177 case Some(parent) => 178 next_elem = get_parent(parent) 179 parent 180 case None => Iterator.empty.next() 181 } 182 } 183 184 def parent_window(component: Component): Option[Window] = 185 ancestors(component).collectFirst({ case x: Window => x }) 186 187 def layered_pane(component: Component): Option[JLayeredPane] = 188 parent_window(component) match { 189 case Some(w: JWindow) => Some(w.getLayeredPane) 190 case Some(w: JFrame) => Some(w.getLayeredPane) 191 case Some(w: JDialog) => Some(w.getLayeredPane) 192 case _ => None 193 } 194 195 def traverse_components(component: Component, apply: Component => Unit) 196 { 197 def traverse(comp: Component) 198 { 199 apply(comp) 200 comp match { 201 case cont: Container => 202 for (i <- 0 until cont.getComponentCount) 203 traverse(cont.getComponent(i)) 204 case _ => 205 } 206 } 207 traverse(component) 208 } 209 210 211 /* font operations */ 212 213 def copy_font(font: Font): Font = 214 if (font == null) null 215 else new Font(font.getFamily, font.getStyle, font.getSize) 216 217 def line_metrics(font: Font): LineMetrics = 218 font.getLineMetrics("", new FontRenderContext(null, false, false)) 219 220 def transform_font(font: Font, transform: AffineTransform): Font = 221 font.deriveFont(java.util.Map.of(TextAttribute.TRANSFORM, new TransformAttribute(transform))) 222 223 def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font = 224 new Font(family, if (bold) Font.BOLD else Font.PLAIN, size) 225 226 def label_font(): Font = (new JLabel).getFont 227 228 229 /* Isabelle fonts */ 230 231 def imitate_font(font: Font, 232 family: String = Isabelle_Fonts.sans, 233 scale: Double = 1.0): Font = 234 { 235 val font1 = new Font(family, font.getStyle, font.getSize) 236 val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight 237 new Font(family, font.getStyle, (scale * rel_size * font.getSize).toInt) 238 } 239 240 def imitate_font_css(font: Font, 241 family: String = Isabelle_Fonts.sans, 242 scale: Double = 1.0): String = 243 { 244 val font1 = new Font(family, font.getStyle, font.getSize) 245 val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight 246 "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;" 247 } 248 249 def use_isabelle_fonts() 250 { 251 val default_font = label_font() 252 val ui = UIManager.getDefaults 253 for (prop <- List( 254 "CheckBoxMenuItem.font", 255 "Label.font", 256 "Menu.font", 257 "MenuItem.font", 258 "PopupMenu.font", 259 "Table.font", 260 "TableHeader.font", 261 "TextArea.font", 262 "TextField.font", 263 "TextPane.font", 264 "ToolTip.font", 265 "Tree.font")) 266 { 267 val font = ui.get(prop) match { case font: Font => font case _ => default_font } 268 ui.put(prop, GUI.imitate_font(font)) 269 } 270 } 271} 272