src/Pure/GUI/gui.scala
changeset 69377 81ae5893c556
parent 69376 53194e2a969d
child 69378 429426640596
     1.1 --- a/src/Pure/GUI/gui.scala	Fri Nov 30 14:21:28 2018 +0100
     1.2 +++ b/src/Pure/GUI/gui.scala	Fri Nov 30 14:46:00 2018 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
     1.5  import java.awt.geom.AffineTransform
     1.6  import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog,
     1.7 -  JButton, JTextField}
     1.8 +  JButton, JTextField, JLabel}
     1.9  
    1.10  import scala.swing.{ComboBox, TextArea, ScrollPane}
    1.11  import scala.swing.event.SelectionChanged
    1.12 @@ -224,6 +224,8 @@
    1.13    def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
    1.14      new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
    1.15  
    1.16 +  def label_font(): Font = (new JLabel).getFont
    1.17 +
    1.18  
    1.19    /* Isabelle fonts */
    1.20  
    1.21 @@ -244,4 +246,15 @@
    1.22      val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
    1.23      "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;"
    1.24    }
    1.25 +
    1.26 +  def use_isabelle_fonts()
    1.27 +  {
    1.28 +    val default_font = label_font()
    1.29 +    val ui = UIManager.getDefaults
    1.30 +    for (prop <- List("Label.font", "TextArea.font", "TextPane.font", "Tooltip.font", "Tree.font"))
    1.31 +    {
    1.32 +      val font = ui.get(prop) match { case font: Font => font case _ => default_font }
    1.33 +      ui.put(prop, GUI.imitate_font(font))
    1.34 +    }
    1.35 +  }
    1.36  }