# HG changeset patch
# User wenzelm
# Date 1308604778 -7200
# Node ID 51b8043a8cf5ee8c3b91c7b3554c61f2fc04fd49
# Parent  a7a8496d3bfcce9e73945094ab23e5cd32485f3d
simplified/generalized ISABELLE_FONTS handling;

diff -r a7a8496d3bfc -r 51b8043a8cf5 etc/settings
--- a/etc/settings	Mon Jun 20 22:48:41 2011 +0200
+++ b/etc/settings	Mon Jun 20 23:19:38 2011 +0200
@@ -188,7 +188,7 @@
 ### Rendering information
 ###
 
-ISABELLE_FONT_FAMILY="IsabelleText"
+ISABELLE_FONTS="$ISABELLE_HOME/lib/fonts/IsabelleText.ttf:$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"
 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
 
 
diff -r a7a8496d3bfc -r 51b8043a8cf5 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Jun 20 22:48:41 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Jun 20 23:19:38 2011 +0200
@@ -390,24 +390,13 @@
 
   /* fonts */
 
-  val font_family = getenv_strict("ISABELLE_FONT_FAMILY")
-  val font_family_default = "IsabelleText"
-
-  def get_font(size: Int = 1, bold: Boolean = false): Font =
-    new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size)
-
-  def create_default_font(bold: Boolean = false): Font =
-    if (bold)
-      Font.createFont(Font.TRUETYPE_FONT,
-        platform_file("$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"))
-    else
-      Font.createFont(Font.TRUETYPE_FONT,
-        platform_file("$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"))
+  def get_font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
+    new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
 
   def install_fonts()
   {
     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
-    ge.registerFont(create_default_font(bold = false))
-    ge.registerFont(create_default_font(bold = true))
+    for (font <- getenv_strict("ISABELLE_FONTS").split(":"))
+      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font)))
   }
 }