# HG changeset patch
# User haftmann
# Date 1260274744 -3600
# Node ID d3dead6ae0d2c3f86a94ff8ff51be9e8f59ec9f3
# Parent  1e620676303635d2acf9c26e40e0bdb504a68735# Parent  7996b488a9b509a3019531a9f71076a28e91c78b
merged

diff -r 1e6206763036 -r d3dead6ae0d2 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Dec 07 16:27:48 2009 +0100
+++ b/src/Pure/System/isabelle_system.scala	Tue Dec 08 13:19:04 2009 +0100
@@ -9,6 +9,7 @@
 import java.util.regex.Pattern
 import java.util.Locale
 import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException}
+import java.awt.{GraphicsEnvironment, Font}
 
 import scala.io.Source
 import scala.util.matching.Regex
@@ -259,7 +260,7 @@
   {
     getenv_strict("ISABELLE_TOOLS").split(":").find(dir => {
       val file = platform_file(dir + "/" + name)
-      try { file.isFile && file.canRead } //  file.canExecute requires Java 1.6
+      try { file.isFile && file.canRead && file.canExecute }
       catch { case _: SecurityException => false }
     }) match {
       case Some(dir) =>
@@ -331,4 +332,20 @@
   val symbols = new Symbol.Interpretation(
     read_symbols("$ISABELLE_HOME/etc/symbols") ++
     read_symbols("$ISABELLE_HOME_USER/etc/symbols"))
+
+
+  /* fonts */
+
+  val font_family = "IsabelleText"
+
+  private def create_font(name: String) =
+    Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
+
+  def register_fonts(): Boolean =
+  {
+    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
+    val ok1 = ge.registerFont(create_font("~~/lib/fonts/IsabelleText.ttf"))
+    val ok2 = ge.registerFont(create_font("~~/lib/fonts/IsabelleTextBold.ttf"))
+    ok1 && ok2
+  }
 }