equal
deleted
inserted
replaced
249 |
249 |
250 def use_isabelle_fonts() |
250 def use_isabelle_fonts() |
251 { |
251 { |
252 val default_font = label_font() |
252 val default_font = label_font() |
253 val ui = UIManager.getDefaults |
253 val ui = UIManager.getDefaults |
254 for (prop <- List("Label.font", "Menu.font", "MenuItem.font", "PopupMenu.font", |
254 for (prop <- List( |
255 "TextArea.font", "TextField.font", "TextPane.font", "Tooltip.font", "Tree.font")) |
255 "CheckBoxMenuItem.font", |
|
256 "Label.font", |
|
257 "Menu.font", |
|
258 "MenuItem.font", |
|
259 "PopupMenu.font", |
|
260 "TextArea.font", |
|
261 "TextField.font", |
|
262 "TextPane.font", |
|
263 "Tooltip.font", |
|
264 "Tree.font")) |
256 { |
265 { |
257 val font = ui.get(prop) match { case font: Font => font case _ => default_font } |
266 val font = ui.get(prop) match { case font: Font => font case _ => default_font } |
258 ui.put(prop, GUI.imitate_font(font)) |
267 ui.put(prop, GUI.imitate_font(font)) |
259 } |
268 } |
260 } |
269 } |