# HG changeset patch
# User wenzelm
# Date 1265412121 -3600
# Node ID 1ea6dba95b49265c3f9b5fa311467706098247d4
# Parent  b90d205a4abf2ffc3dba0cf745c69c0ffc78753b
tuned font handling;
explicit workaround for Apple's font manager in Java 1.6, which fails to create "IsabelleTextBold" as family member of "IsabelleText";

diff -r b90d205a4abf -r 1ea6dba95b49 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Feb 05 22:09:57 2010 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Feb 06 00:22:01 2010 +0100
@@ -310,20 +310,29 @@
 
   val font_family = "IsabelleText"
 
-  private def check_font(): Boolean =
-    new Font(font_family, Font.PLAIN, 1).getFamily == font_family
-
-  private def create_font(name: String) =
-    Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
+  def get_font(bold: Boolean): Font =
+    new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, 1)
 
   def install_fonts()
   {
+    def create_font(bold: Boolean): Font =
+    {
+      val name =
+        if (bold) "$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"
+        else "$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"
+      Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
+    }
+    def check_font() = get_font(false).getFamily == font_family
+
     if (!check_font()) {
+      val font = create_font(false)
+      val bold_font = create_font(true)
+
       val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
-      ge.registerFont(create_font("$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"))
-      ge.registerFont(create_font("$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"))
-      if (!check_font())
-        error("Failed to install IsabelleText fonts")
+      ge.registerFont(font)
+      // workaround strange problem with Apple's Java 1.6 font manager
+      if (bold_font.getFamily == font_family) ge.registerFont(bold_font)
+      if (!check_font()) error("Failed to install IsabelleText fonts")
     }
   }
 }