clarified font_family vs. font_family_default;
authorwenzelm
Tue, 08 Jun 2010 17:45:39 +0200
changeset 374688680677265c9
parent 37467 5c6695de35ba
child 37469 1c816f2abb0e
clarified font_family vs. font_family_default;
install_fonts: refrain from any magic that does not really work on Mac OS, but introduces strange problems on other platforms;
src/Pure/System/isabelle_system.scala
     1.1 --- a/src/Pure/System/isabelle_system.scala	Tue Jun 08 13:51:25 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_system.scala	Tue Jun 08 17:45:39 2010 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4    BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
     1.5    File, IOException}
     1.6  import java.awt.{GraphicsEnvironment, Font}
     1.7 +import java.awt.font.TextAttribute
     1.8  
     1.9  import scala.io.Source
    1.10  import scala.util.matching.Regex
    1.11 @@ -336,31 +337,23 @@
    1.12    /* fonts */
    1.13  
    1.14    val font_family = getenv_strict("ISABELLE_FONT_FAMILY")
    1.15 +  val font_family_default = "IsabelleText"
    1.16  
    1.17    def get_font(size: Int = 1, bold: Boolean = false): Font =
    1.18      new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size)
    1.19  
    1.20 +  def create_default_font(bold: Boolean = false): Font =
    1.21 +    if (bold)
    1.22 +      Font.createFont(Font.TRUETYPE_FONT,
    1.23 +        platform_file("$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"))
    1.24 +    else
    1.25 +      Font.createFont(Font.TRUETYPE_FONT,
    1.26 +        platform_file("$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"))
    1.27 +
    1.28    def install_fonts()
    1.29    {
    1.30 -    def create_font(bold: Boolean): Font =
    1.31 -    {
    1.32 -      val name =
    1.33 -        if (bold) "$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"
    1.34 -        else "$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"
    1.35 -      Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
    1.36 -    }
    1.37 -    def check_font() = get_font().getFamily == font_family
    1.38 -
    1.39 -    if (!check_font()) {
    1.40 -      val font = create_font(false)
    1.41 -      val bold_font = create_font(true)
    1.42 -
    1.43 -      val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
    1.44 -      ge.registerFont(font)
    1.45 -      // workaround strange problem with Apple's Java 1.6 font manager
    1.46 -      // FIXME does not quite work!?
    1.47 -      if (bold_font.getFamily == font_family) ge.registerFont(bold_font)
    1.48 -      if (!check_font()) error("Failed to install IsabelleText fonts")
    1.49 -    }
    1.50 +    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
    1.51 +    ge.registerFont(create_default_font(bold = false))
    1.52 +    ge.registerFont(create_default_font(bold = true))
    1.53    }
    1.54  }