|
1 /* Title: Pure/System/gui.scala |
|
2 Author: Makarius |
|
3 |
|
4 Elementary GUI tools. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 import java.awt.{Image, Component, Toolkit} |
|
11 import javax.swing.{ImageIcon, JOptionPane, UIManager} |
|
12 |
|
13 import scala.swing.{ComboBox, TextArea, ScrollPane} |
|
14 import scala.swing.event.SelectionChanged |
|
15 |
|
16 |
|
17 object GUI |
|
18 { |
|
19 /* Swing look-and-feel */ |
|
20 |
|
21 def get_laf(): String = |
|
22 { |
|
23 def laf(name: String): Option[String] = |
|
24 UIManager.getInstalledLookAndFeels().find(_.getName == name).map(_.getClassName) |
|
25 |
|
26 if (Platform.is_windows || Platform.is_macos) |
|
27 UIManager.getSystemLookAndFeelClassName() |
|
28 else |
|
29 laf("Nimbus") orElse laf("GTK+") getOrElse |
|
30 UIManager.getCrossPlatformLookAndFeelClassName() |
|
31 } |
|
32 |
|
33 def init_laf(): Unit = UIManager.setLookAndFeel(get_laf()) |
|
34 |
|
35 |
|
36 /* simple dialogs */ |
|
37 |
|
38 def scrollable_text(txt: String, width: Int = 60, editable: Boolean = false): ScrollPane = |
|
39 { |
|
40 val text = new TextArea(txt) |
|
41 if (width > 0) text.columns = width |
|
42 text.editable = editable |
|
43 new ScrollPane(text) |
|
44 } |
|
45 |
|
46 private def simple_dialog(kind: Int, default_title: String, |
|
47 parent: Component, title: String, message: Seq[Any]) |
|
48 { |
|
49 Swing_Thread.now { |
|
50 val java_message = message map { case x: scala.swing.Component => x.peer case x => x } |
|
51 JOptionPane.showMessageDialog(parent, |
|
52 java_message.toArray.asInstanceOf[Array[AnyRef]], |
|
53 if (title == null) default_title else title, kind) |
|
54 } |
|
55 } |
|
56 |
|
57 def dialog(parent: Component, title: String, message: Any*) = |
|
58 simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message) |
|
59 |
|
60 def warning_dialog(parent: Component, title: String, message: Any*) = |
|
61 simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message) |
|
62 |
|
63 def error_dialog(parent: Component, title: String, message: Any*) = |
|
64 simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message) |
|
65 |
|
66 def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int = |
|
67 Swing_Thread.now { |
|
68 val java_message = message map { case x: scala.swing.Component => x.peer case x => x } |
|
69 JOptionPane.showConfirmDialog(parent, |
|
70 java_message.toArray.asInstanceOf[Array[AnyRef]], title, |
|
71 option_type, JOptionPane.QUESTION_MESSAGE) |
|
72 } |
|
73 |
|
74 |
|
75 /* zoom box */ |
|
76 |
|
77 class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String]( |
|
78 List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) |
|
79 { |
|
80 val Factor = "([0-9]+)%?".r |
|
81 def parse(text: String): Int = |
|
82 text match { |
|
83 case Factor(s) => |
|
84 val i = Integer.parseInt(s) |
|
85 if (10 <= i && i <= 1000) i else 100 |
|
86 case _ => 100 |
|
87 } |
|
88 |
|
89 def print(i: Int): String = i.toString + "%" |
|
90 |
|
91 def set_item(i: Int) { |
|
92 peer.getEditor match { |
|
93 case null => |
|
94 case editor => editor.setItem(print(i)) |
|
95 } |
|
96 } |
|
97 |
|
98 makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x)) |
|
99 reactions += { |
|
100 case SelectionChanged(_) => apply_factor(parse(selection.item)) |
|
101 } |
|
102 listenTo(selection) |
|
103 selection.index = 3 |
|
104 prototypeDisplayValue = Some("00000%") |
|
105 } |
|
106 |
|
107 |
|
108 /* screen resolution */ |
|
109 |
|
110 def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72 |
|
111 def resolution_scale(i: Int): Int = (i.toDouble * resolution_scale()).round.toInt |
|
112 |
|
113 |
|
114 /* icon */ |
|
115 |
|
116 def isabelle_icon(): ImageIcon = |
|
117 new ImageIcon(Isabelle_System.platform_path(Path.explode("~~/lib/logo/isabelle.gif"))) |
|
118 |
|
119 def isabelle_image(): Image = isabelle_icon().getImage |
|
120 } |
|
121 |