# HG changeset patch
# User wenzelm
# Date 1543586551 -3600
# Node ID 42942664059615f509cae3644f4f93354357fcf6
# Parent  81ae5893c556023e10c31e1546bd8b5c9229076e
more Isabelle fonts;

diff -r 81ae5893c556 -r 429426640596 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Fri Nov 30 14:46:00 2018 +0100
+++ b/src/Pure/GUI/gui.scala	Fri Nov 30 15:02:31 2018 +0100
@@ -251,7 +251,8 @@
   {
     val default_font = label_font()
     val ui = UIManager.getDefaults
-    for (prop <- List("Label.font", "TextArea.font", "TextPane.font", "Tooltip.font", "Tree.font"))
+    for (prop <- List("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))