--- a/src/Pure/GUI/gui.scala Sat Dec 01 16:11:59 2018 +0100
+++ b/src/Pure/GUI/gui.scala Sat Dec 01 16:57:46 2018 +0100
@@ -251,8 +251,17 @@
{
val default_font = label_font()
val ui = UIManager.getDefaults
- for (prop <- List("Label.font", "Menu.font", "MenuItem.font", "PopupMenu.font",
- "TextArea.font", "TextField.font", "TextPane.font", "Tooltip.font", "Tree.font"))
+ for (prop <- List(
+ "CheckBoxMenuItem.font",
+ "Label.font",
+ "Menu.font",
+ "MenuItem.font",
+ "PopupMenu.font",
+ "TextArea.font",
+ "TextField.font",
+ "TextPane.font",
+ "Tooltip.font",
+ "Tree.font"))
{
val font = ui.get(prop) match { case font: Font => font case _ => default_font }
ui.put(prop, GUI.imitate_font(font))