# HG changeset patch
# User wenzelm
# Date 1543679866 -3600
# Node ID 0c7d8b1b659432a8aaa0132264cf3329a9a50f0d
# Parent  747f8b052e591cf07bc4a48c581504b3e8e23644
more Isabelle fonts: CheckBoxMenuItem.font notably for Windows L&F;

diff -r 747f8b052e59 -r 0c7d8b1b6594 src/Pure/GUI/gui.scala
--- 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))