more Isabelle fonts;
authorwenzelm
Fri Nov 30 15:02:31 2018 +0100 (12 months ago)
changeset 69378429426640596
parent 69377 81ae5893c556
child 69379 5082e843b726
more Isabelle fonts;
src/Pure/GUI/gui.scala
     1.1 --- a/src/Pure/GUI/gui.scala	Fri Nov 30 14:46:00 2018 +0100
     1.2 +++ b/src/Pure/GUI/gui.scala	Fri Nov 30 15:02:31 2018 +0100
     1.3 @@ -251,7 +251,8 @@
     1.4    {
     1.5      val default_font = label_font()
     1.6      val ui = UIManager.getDefaults
     1.7 -    for (prop <- List("Label.font", "TextArea.font", "TextPane.font", "Tooltip.font", "Tree.font"))
     1.8 +    for (prop <- List("Label.font", "Menu.font", "MenuItem.font", "PopupMenu.font",
     1.9 +      "TextArea.font", "TextField.font", "TextPane.font", "Tooltip.font", "Tree.font"))
    1.10      {
    1.11        val font = ui.get(prop) match { case font: Font => font case _ => default_font }
    1.12        ui.put(prop, GUI.imitate_font(font))