author | wenzelm |
Tue, 05 Jan 2021 21:58:00 +0100 | |
changeset 73072 | 7460f92d63fc |
parent 73070 | 7ef8d77ee761 |
child 73073 | a1d4c9f5207a |
permissions | -rw-r--r-- |
53783
f5e9d182f645
clarified location of GUI modules (which depend on Swing of JFX);
wenzelm
parents:
53778
diff
changeset
|
1 |
/* Title: Pure/GUI/gui.scala |
51619 | 2 |
Author: Makarius |
3 |
||
53712 | 4 |
Basic GUI tools (for AWT/Swing). |
51619 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
73037 | 9 |
import java.awt.{Component, Container, Font, Image, Insets, KeyboardFocusManager, Window, Point, |
73072 | 10 |
Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit, Taskbar} |
72974 | 11 |
import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute} |
53785 | 12 |
import java.awt.geom.AffineTransform |
72974 | 13 |
import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane, |
14 |
JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities} |
|
15 |
import scala.swing.{ComboBox, ScrollPane, TextArea} |
|
51619 | 16 |
import scala.swing.event.SelectionChanged |
17 |
||
18 |
||
19 |
object GUI |
|
20 |
{ |
|
21 |
/* Swing look-and-feel */ |
|
22 |
||
59201
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59183
diff
changeset
|
23 |
def find_laf(name: String): Option[String] = |
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59183
diff
changeset
|
24 |
UIManager.getInstalledLookAndFeels(). |
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59183
diff
changeset
|
25 |
find(c => c.getName == name || c.getClassName == name). |
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59183
diff
changeset
|
26 |
map(_.getClassName) |
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59183
diff
changeset
|
27 |
|
51619 | 28 |
def get_laf(): String = |
59201
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59183
diff
changeset
|
29 |
find_laf(System.getProperty("isabelle.laf")) getOrElse { |
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59183
diff
changeset
|
30 |
if (Platform.is_windows || Platform.is_macos) |
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59183
diff
changeset
|
31 |
UIManager.getSystemLookAndFeelClassName() |
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59183
diff
changeset
|
32 |
else |
61529
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61523
diff
changeset
|
33 |
UIManager.getCrossPlatformLookAndFeelClassName() |
59201
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59183
diff
changeset
|
34 |
} |
51619 | 35 |
|
36 |
def init_laf(): Unit = UIManager.setLookAndFeel(get_laf()) |
|
37 |
||
72975 | 38 |
def current_laf(): String = UIManager.getLookAndFeel.getClass.getName() |
39 |
||
53848
8d7029eb0c31
disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly;
wenzelm
parents:
53786
diff
changeset
|
40 |
def is_macos_laf(): Boolean = |
72975 | 41 |
Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf() |
53848
8d7029eb0c31
disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly;
wenzelm
parents:
53786
diff
changeset
|
42 |
|
60998 | 43 |
def is_windows_laf(): Boolean = |
72975 | 44 |
Platform.is_windows && UIManager.getSystemLookAndFeelClassName() == current_laf() |
60998 | 45 |
|
51619 | 46 |
|
56752
72b4205f4de9
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
wenzelm
parents:
56622
diff
changeset
|
47 |
/* plain focus traversal, notably for text fields */ |
72b4205f4de9
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
wenzelm
parents:
56622
diff
changeset
|
48 |
|
72b4205f4de9
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
wenzelm
parents:
56622
diff
changeset
|
49 |
def plain_focus_traversal(component: Component) |
72b4205f4de9
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
wenzelm
parents:
56622
diff
changeset
|
50 |
{ |
72b4205f4de9
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
wenzelm
parents:
56622
diff
changeset
|
51 |
val dummy_button = new JButton |
72b4205f4de9
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
wenzelm
parents:
56622
diff
changeset
|
52 |
def apply(id: Int): Unit = |
72b4205f4de9
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
wenzelm
parents:
56622
diff
changeset
|
53 |
component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id)) |
72b4205f4de9
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
wenzelm
parents:
56622
diff
changeset
|
54 |
apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS) |
72b4205f4de9
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
wenzelm
parents:
56622
diff
changeset
|
55 |
apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS) |
72b4205f4de9
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
wenzelm
parents:
56622
diff
changeset
|
56 |
} |
72b4205f4de9
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
wenzelm
parents:
56622
diff
changeset
|
57 |
|
72b4205f4de9
uniform focus traversal via TAB / Shift-TAB for all fields, in contrast to Java defaults, but in accordance to occasional jEdit practice;
wenzelm
parents:
56622
diff
changeset
|
58 |
|
51619 | 59 |
/* simple dialogs */ |
60 |
||
59671
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59286
diff
changeset
|
61 |
def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false) |
53714 | 62 |
: ScrollPane = |
51619 | 63 |
{ |
59671
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
59286
diff
changeset
|
64 |
val txt = Output.clean_yxml(raw_txt) |
51619 | 65 |
val text = new TextArea(txt) |
66 |
if (width > 0) text.columns = width |
|
53714 | 67 |
if (height > 0 && split_lines(txt).length > height) text.rows = height |
51619 | 68 |
text.editable = editable |
69 |
new ScrollPane(text) |
|
70 |
} |
|
71 |
||
72 |
private def simple_dialog(kind: Int, default_title: String, |
|
65370 | 73 |
parent: Component, title: String, message: Iterable[Any]) |
51619 | 74 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
75 |
GUI_Thread.now { |
65370 | 76 |
val java_message = |
77 |
message.iterator.map({ case x: scala.swing.Component => x.peer case x => x }). |
|
78 |
toArray.asInstanceOf[Array[AnyRef]] |
|
79 |
JOptionPane.showMessageDialog(parent, java_message, |
|
51619 | 80 |
if (title == null) default_title else title, kind) |
81 |
} |
|
82 |
} |
|
83 |
||
57639 | 84 |
def dialog(parent: Component, title: String, message: Any*): Unit = |
51619 | 85 |
simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message) |
86 |
||
57639 | 87 |
def warning_dialog(parent: Component, title: String, message: Any*): Unit = |
51619 | 88 |
simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message) |
89 |
||
57639 | 90 |
def error_dialog(parent: Component, title: String, message: Any*): Unit = |
51619 | 91 |
simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message) |
92 |
||
93 |
def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int = |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
94 |
GUI_Thread.now { |
51619 | 95 |
val java_message = message map { case x: scala.swing.Component => x.peer case x => x } |
96 |
JOptionPane.showConfirmDialog(parent, |
|
97 |
java_message.toArray.asInstanceOf[Array[AnyRef]], title, |
|
98 |
option_type, JOptionPane.QUESTION_MESSAGE) |
|
99 |
} |
|
100 |
||
101 |
||
102 |
/* zoom box */ |
|
103 |
||
57044 | 104 |
private val Zoom_Factor = "([0-9]+)%?".r |
105 |
||
106 |
abstract class Zoom_Box extends ComboBox[String]( |
|
51619 | 107 |
List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) |
108 |
{ |
|
57044 | 109 |
def changed: Unit |
110 |
def factor: Int = parse(selection.item) |
|
111 |
||
112 |
private def parse(text: String): Int = |
|
51619 | 113 |
text match { |
57044 | 114 |
case Zoom_Factor(s) => |
51619 | 115 |
val i = Integer.parseInt(s) |
56874 | 116 |
if (10 <= i && i < 1000) i else 100 |
51619 | 117 |
case _ => 100 |
118 |
} |
|
119 |
||
57044 | 120 |
private def print(i: Int): String = i.toString + "%" |
51619 | 121 |
|
122 |
def set_item(i: Int) { |
|
123 |
peer.getEditor match { |
|
124 |
case null => |
|
125 |
case editor => editor.setItem(print(i)) |
|
126 |
} |
|
127 |
} |
|
128 |
||
129 |
makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x)) |
|
56874 | 130 |
peer.getEditor.getEditorComponent match { |
56888 | 131 |
case text: JTextField => text.setColumns(4) |
56874 | 132 |
case _ => |
133 |
} |
|
134 |
||
57044 | 135 |
selection.index = 3 |
136 |
||
51619 | 137 |
listenTo(selection) |
57044 | 138 |
reactions += { case SelectionChanged(_) => changed } |
51619 | 139 |
} |
140 |
||
141 |
||
53786 | 142 |
/* tooltip with multi-line support */ |
143 |
||
56622
891d1b8b64fb
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents:
54965
diff
changeset
|
144 |
def tooltip_lines(text: String): String = |
891d1b8b64fb
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents:
54965
diff
changeset
|
145 |
if (text == null || text == "") null |
62113 | 146 |
else "<html>" + HTML.output(text) + "</html>" |
53786 | 147 |
|
148 |
||
51619 | 149 |
/* icon */ |
150 |
||
151 |
def isabelle_icon(): ImageIcon = |
|
54676
6b2ca4850b71
uniform use of transparent icons, as for main "apps";
wenzelm
parents:
54659
diff
changeset
|
152 |
new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle_transparent-32.gif")) |
51619 | 153 |
|
54709 | 154 |
def isabelle_icons(): List[ImageIcon] = |
155 |
for (icon <- List("isabelle/isabelle_transparent-32.gif", "isabelle/isabelle_transparent.gif")) |
|
156 |
yield new ImageIcon(getClass.getClassLoader.getResource(icon)) |
|
157 |
||
51619 | 158 |
def isabelle_image(): Image = isabelle_icon().getImage |
53712 | 159 |
|
73070 | 160 |
def isabelle_image_large(): Image = |
161 |
Toolkit.getDefaultToolkit.getImage( |
|
162 |
File.platform_path(Path.explode("~~/lib/logo/isabelle_transparent-128.png"))) |
|
163 |
||
164 |
def set_application_icon() |
|
165 |
{ |
|
166 |
if (Platform.is_macos) { |
|
73072 | 167 |
Taskbar.getTaskbar.setIconImage(isabelle_image_large()) |
73070 | 168 |
} |
169 |
} |
|
170 |
||
53712 | 171 |
|
72974 | 172 |
/* location within multi-screen environment */ |
173 |
||
174 |
final case class Screen_Location(point: Point, bounds: Rectangle) |
|
175 |
{ |
|
176 |
def relative(parent: Component, size: Dimension): Point = |
|
177 |
{ |
|
178 |
val w = size.width |
|
179 |
val h = size.height |
|
180 |
||
181 |
val x0 = parent.getLocationOnScreen.x |
|
182 |
val y0 = parent.getLocationOnScreen.y |
|
183 |
val x1 = x0 + parent.getWidth - w |
|
184 |
val y1 = y0 + parent.getHeight - h |
|
185 |
val x2 = point.x min (bounds.x + bounds.width - w) |
|
186 |
val y2 = point.y min (bounds.y + bounds.height - h) |
|
187 |
||
188 |
val location = new Point((x2 min x1) max x0, (y2 min y1) max y0) |
|
189 |
SwingUtilities.convertPointFromScreen(location, parent) |
|
190 |
location |
|
191 |
} |
|
192 |
} |
|
193 |
||
194 |
def screen_location(component: Component, point: Point): Screen_Location = |
|
195 |
{ |
|
196 |
val screen_point = new Point(point.x, point.y) |
|
197 |
if (component != null) SwingUtilities.convertPointToScreen(screen_point, component) |
|
198 |
||
199 |
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment |
|
200 |
val screen_bounds = |
|
201 |
(for { |
|
202 |
device <- ge.getScreenDevices.iterator |
|
203 |
config <- device.getConfigurations.iterator |
|
204 |
bounds = config.getBounds |
|
205 |
} yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds |
|
206 |
||
207 |
Screen_Location(screen_point, screen_bounds) |
|
208 |
} |
|
209 |
||
210 |
def mouse_location(): Screen_Location = |
|
211 |
screen_location(null, MouseInfo.getPointerInfo.getLocation) |
|
212 |
||
213 |
||
73037 | 214 |
/* screen size */ |
215 |
||
216 |
sealed case class Screen_Size(bounds: Rectangle, insets: Insets) |
|
217 |
{ |
|
73038
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
218 |
def full_screen_bounds: Rectangle = |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
219 |
if (Platform.is_linux) { |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
220 |
// avoid menu bar and docking areas |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
221 |
new Rectangle( |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
222 |
bounds.x + insets.left, |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
223 |
bounds.y + insets.top, |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
224 |
bounds.width - insets.left - insets.right, |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
225 |
bounds.height - insets.top - insets.bottom) |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
226 |
} |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
227 |
else if (Platform.is_macos) { |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
228 |
// avoid menu bar, but ignore docking areas |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
229 |
new Rectangle( |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
230 |
bounds.x, |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
231 |
bounds.y + insets.top, |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
232 |
bounds.width, |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
233 |
bounds.height - insets.top) |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
234 |
} |
3b14f7315dd2
some attempts at multi-platform full-screen mode;
wenzelm
parents:
73037
diff
changeset
|
235 |
else bounds |
73037 | 236 |
} |
237 |
||
238 |
def screen_size(component: Component): Screen_Size = |
|
239 |
{ |
|
240 |
val config = component.getGraphicsConfiguration |
|
241 |
val bounds = config.getBounds |
|
242 |
val insets = Toolkit.getDefaultToolkit.getScreenInsets(config) |
|
243 |
Screen_Size(bounds, insets) |
|
244 |
} |
|
245 |
||
246 |
||
53712 | 247 |
/* component hierachy */ |
248 |
||
249 |
def get_parent(component: Component): Option[Container] = |
|
250 |
component.getParent match { |
|
251 |
case null => None |
|
252 |
case parent => Some(parent) |
|
253 |
} |
|
254 |
||
255 |
def ancestors(component: Component): Iterator[Container] = new Iterator[Container] { |
|
256 |
private var next_elem = get_parent(component) |
|
257 |
def hasNext(): Boolean = next_elem.isDefined |
|
258 |
def next(): Container = |
|
259 |
next_elem match { |
|
260 |
case Some(parent) => |
|
261 |
next_elem = get_parent(parent) |
|
262 |
parent |
|
263 |
case None => Iterator.empty.next() |
|
264 |
} |
|
265 |
} |
|
266 |
||
267 |
def parent_window(component: Component): Option[Window] = |
|
268 |
ancestors(component).collectFirst({ case x: Window => x }) |
|
53778
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53714
diff
changeset
|
269 |
|
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53714
diff
changeset
|
270 |
def layered_pane(component: Component): Option[JLayeredPane] = |
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53714
diff
changeset
|
271 |
parent_window(component) match { |
57879
91e188508bc9
proper layered_pane for JDialog, e.g. relevant for floating dockables in jEdit, for completion popup in text field;
wenzelm
parents:
57639
diff
changeset
|
272 |
case Some(w: JWindow) => Some(w.getLayeredPane) |
91e188508bc9
proper layered_pane for JDialog, e.g. relevant for floating dockables in jEdit, for completion popup in text field;
wenzelm
parents:
57639
diff
changeset
|
273 |
case Some(w: JFrame) => Some(w.getLayeredPane) |
91e188508bc9
proper layered_pane for JDialog, e.g. relevant for floating dockables in jEdit, for completion popup in text field;
wenzelm
parents:
57639
diff
changeset
|
274 |
case Some(w: JDialog) => Some(w.getLayeredPane) |
53778
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53714
diff
changeset
|
275 |
case _ => None |
29eaacff4078
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
wenzelm
parents:
53714
diff
changeset
|
276 |
} |
53785 | 277 |
|
63874 | 278 |
def traverse_components(component: Component, apply: Component => Unit) |
279 |
{ |
|
280 |
def traverse(comp: Component) |
|
281 |
{ |
|
282 |
apply(comp) |
|
283 |
comp match { |
|
284 |
case cont: Container => |
|
285 |
for (i <- 0 until cont.getComponentCount) |
|
286 |
traverse(cont.getComponent(i)) |
|
287 |
case _ => |
|
288 |
} |
|
289 |
} |
|
290 |
traverse(component) |
|
291 |
} |
|
292 |
||
53785 | 293 |
|
294 |
/* font operations */ |
|
295 |
||
61742
fd3b214b0979
clarified font: GUI defaults might change dynamically;
wenzelm
parents:
61529
diff
changeset
|
296 |
def copy_font(font: Font): Font = |
fd3b214b0979
clarified font: GUI defaults might change dynamically;
wenzelm
parents:
61529
diff
changeset
|
297 |
if (font == null) null |
fd3b214b0979
clarified font: GUI defaults might change dynamically;
wenzelm
parents:
61529
diff
changeset
|
298 |
else new Font(font.getFamily, font.getStyle, font.getSize) |
fd3b214b0979
clarified font: GUI defaults might change dynamically;
wenzelm
parents:
61529
diff
changeset
|
299 |
|
59230 | 300 |
def line_metrics(font: Font): LineMetrics = |
53785 | 301 |
font.getLineMetrics("", new FontRenderContext(null, false, false)) |
302 |
||
69376 | 303 |
def transform_font(font: Font, transform: AffineTransform): Font = |
71357 | 304 |
font.deriveFont(java.util.Map.of(TextAttribute.TRANSFORM, new TransformAttribute(transform))) |
69376 | 305 |
|
306 |
def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font = |
|
307 |
new Font(family, if (bold) Font.BOLD else Font.PLAIN, size) |
|
308 |
||
69377 | 309 |
def label_font(): Font = (new JLabel).getFont |
310 |
||
69376 | 311 |
|
312 |
/* Isabelle fonts */ |
|
313 |
||
69358
71ef6e6da3dc
prefer Isabelle_Fonts.sans (not mono) as derived GUI font;
wenzelm
parents:
69357
diff
changeset
|
314 |
def imitate_font(font: Font, |
71ef6e6da3dc
prefer Isabelle_Fonts.sans (not mono) as derived GUI font;
wenzelm
parents:
69357
diff
changeset
|
315 |
family: String = Isabelle_Fonts.sans, |
71ef6e6da3dc
prefer Isabelle_Fonts.sans (not mono) as derived GUI font;
wenzelm
parents:
69357
diff
changeset
|
316 |
scale: Double = 1.0): Font = |
53785 | 317 |
{ |
318 |
val font1 = new Font(family, font.getStyle, font.getSize) |
|
59286
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59230
diff
changeset
|
319 |
val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight |
ac74eedb910a
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
wenzelm
parents:
59230
diff
changeset
|
320 |
new Font(family, font.getStyle, (scale * rel_size * font.getSize).toInt) |
59183
ec83638b6bfb
imitate font more carefully: err on smaller size;
wenzelm
parents:
59080
diff
changeset
|
321 |
} |
ec83638b6bfb
imitate font more carefully: err on smaller size;
wenzelm
parents:
59080
diff
changeset
|
322 |
|
69358
71ef6e6da3dc
prefer Isabelle_Fonts.sans (not mono) as derived GUI font;
wenzelm
parents:
69357
diff
changeset
|
323 |
def imitate_font_css(font: Font, |
71ef6e6da3dc
prefer Isabelle_Fonts.sans (not mono) as derived GUI font;
wenzelm
parents:
69357
diff
changeset
|
324 |
family: String = Isabelle_Fonts.sans, |
71ef6e6da3dc
prefer Isabelle_Fonts.sans (not mono) as derived GUI font;
wenzelm
parents:
69357
diff
changeset
|
325 |
scale: Double = 1.0): String = |
59183
ec83638b6bfb
imitate font more carefully: err on smaller size;
wenzelm
parents:
59080
diff
changeset
|
326 |
{ |
ec83638b6bfb
imitate font more carefully: err on smaller size;
wenzelm
parents:
59080
diff
changeset
|
327 |
val font1 = new Font(family, font.getStyle, font.getSize) |
59230 | 328 |
val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight |
59183
ec83638b6bfb
imitate font more carefully: err on smaller size;
wenzelm
parents:
59080
diff
changeset
|
329 |
"font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;" |
53785 | 330 |
} |
69377 | 331 |
|
332 |
def use_isabelle_fonts() |
|
333 |
{ |
|
334 |
val default_font = label_font() |
|
335 |
val ui = UIManager.getDefaults |
|
69384
0c7d8b1b6594
more Isabelle fonts: CheckBoxMenuItem.font notably for Windows L&F;
wenzelm
parents:
69378
diff
changeset
|
336 |
for (prop <- List( |
72786
21ff9c1a4644
more Isabelle fonts, notably for PanelWindowContainer buttons with Windows L&F;
wenzelm
parents:
71361
diff
changeset
|
337 |
"ToggleButton.font", |
69384
0c7d8b1b6594
more Isabelle fonts: CheckBoxMenuItem.font notably for Windows L&F;
wenzelm
parents:
69378
diff
changeset
|
338 |
"CheckBoxMenuItem.font", |
0c7d8b1b6594
more Isabelle fonts: CheckBoxMenuItem.font notably for Windows L&F;
wenzelm
parents:
69378
diff
changeset
|
339 |
"Label.font", |
0c7d8b1b6594
more Isabelle fonts: CheckBoxMenuItem.font notably for Windows L&F;
wenzelm
parents:
69378
diff
changeset
|
340 |
"Menu.font", |
0c7d8b1b6594
more Isabelle fonts: CheckBoxMenuItem.font notably for Windows L&F;
wenzelm
parents:
69378
diff
changeset
|
341 |
"MenuItem.font", |
0c7d8b1b6594
more Isabelle fonts: CheckBoxMenuItem.font notably for Windows L&F;
wenzelm
parents:
69378
diff
changeset
|
342 |
"PopupMenu.font", |
71360
fcf5ee85743d
more Isabelle fonts, notably for File Browser title in GTK L&F;
wenzelm
parents:
71357
diff
changeset
|
343 |
"Table.font", |
fcf5ee85743d
more Isabelle fonts, notably for File Browser title in GTK L&F;
wenzelm
parents:
71357
diff
changeset
|
344 |
"TableHeader.font", |
69384
0c7d8b1b6594
more Isabelle fonts: CheckBoxMenuItem.font notably for Windows L&F;
wenzelm
parents:
69378
diff
changeset
|
345 |
"TextArea.font", |
0c7d8b1b6594
more Isabelle fonts: CheckBoxMenuItem.font notably for Windows L&F;
wenzelm
parents:
69378
diff
changeset
|
346 |
"TextField.font", |
0c7d8b1b6594
more Isabelle fonts: CheckBoxMenuItem.font notably for Windows L&F;
wenzelm
parents:
69378
diff
changeset
|
347 |
"TextPane.font", |
71361 | 348 |
"ToolTip.font", |
69384
0c7d8b1b6594
more Isabelle fonts: CheckBoxMenuItem.font notably for Windows L&F;
wenzelm
parents:
69378
diff
changeset
|
349 |
"Tree.font")) |
69377 | 350 |
{ |
351 |
val font = ui.get(prop) match { case font: Font => font case _ => default_font } |
|
352 |
ui.put(prop, GUI.imitate_font(font)) |
|
353 |
} |
|
354 |
} |
|
51619 | 355 |
} |