# HG changeset patch
# User wenzelm
# Date 1365089584 -7200
# Node ID 22d1dd43f08915e9634586f46237c90d3ce0e089
# Parent  81f8da412b7f53e7daf6f5c91e63baa813febf0a
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;

diff -r 81f8da412b7f -r 22d1dd43f089 src/Pure/System/isabelle_font.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_font.scala	Thu Apr 04 17:33:04 2013 +0200
@@ -0,0 +1,35 @@
+/*  Title:      Pure/System/isabelle_font.scala
+    Author:     Makarius
+
+Isabelle font support.
+*/
+
+package isabelle
+
+import java.awt.{GraphicsEnvironment, Font}
+import java.io.{FileInputStream, BufferedInputStream}
+import javafx.scene.text.{Font => JFX_Font}
+
+
+object Isabelle_Font
+{
+  def apply(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()
+    for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
+      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
+  }
+
+  def install_fonts_jfx()
+  {
+    for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS"))) {
+      val stream = new BufferedInputStream(new FileInputStream(font.file))
+      try { JFX_Font.loadFont(stream, 1.0) }
+      finally { stream.close }
+    }
+  }
+}
+
diff -r 81f8da412b7f -r 22d1dd43f089 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Apr 04 17:16:51 2013 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Apr 04 17:33:04 2013 +0200
@@ -9,13 +9,10 @@
 
 import java.lang.System
 import java.util.regex.Pattern
-import java.io.{InputStream, OutputStream, File => JFile, BufferedReader, InputStreamReader,
-  BufferedWriter, OutputStreamWriter, IOException, FileInputStream, BufferedInputStream}
-import java.awt.{GraphicsEnvironment, Font}
-import java.awt.font.TextAttribute
+import java.io.{File => JFile, BufferedReader, InputStreamReader,
+  BufferedWriter, OutputStreamWriter}
 import javax.swing.ImageIcon
 
-import scala.io.Source
 import scala.util.matching.Regex
 
 
@@ -426,28 +423,6 @@
   }
 
 
-  /* fonts */
-
-  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()
-    for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
-      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
-  }
-
-  def install_fonts_jfx()
-  {
-    for (font <- Path.split(getenv_strict("ISABELLE_FONTS"))) {
-      val stream = new BufferedInputStream(new FileInputStream(font.file))
-      try { javafx.scene.text.Font.loadFont(stream, 1.0) }
-      finally { stream.close }
-    }
-  }
-
-
   /* icon */
 
   def get_icon(): ImageIcon =
diff -r 81f8da412b7f -r 22d1dd43f089 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Apr 04 17:16:51 2013 +0200
+++ b/src/Pure/build-jars	Thu Apr 04 17:33:04 2013 +0200
@@ -47,6 +47,7 @@
   System/interrupt.scala
   System/invoke_scala.scala
   System/isabelle_charset.scala
+  System/isabelle_font.scala
   System/isabelle_process.scala
   System/isabelle_system.scala
   System/jfx_thread.scala
diff -r 81f8da412b7f -r 22d1dd43f089 src/Tools/Graphview/src/graphview.scala
--- a/src/Tools/Graphview/src/graphview.scala	Thu Apr 04 17:16:51 2013 +0200
+++ b/src/Tools/Graphview/src/graphview.scala	Thu Apr 04 17:33:04 2013 +0200
@@ -24,7 +24,7 @@
       try {
         Platform.init_laf()
         Isabelle_System.init()
-        Isabelle_System.install_fonts()
+        Isabelle_Font.install_fonts()
         ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
 
         args.toList match {
diff -r 81f8da412b7f -r 22d1dd43f089 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Apr 04 17:16:51 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Apr 04 17:33:04 2013 +0200
@@ -284,7 +284,7 @@
 
       PIDE.plugin = this
       Isabelle_System.init()
-      Isabelle_System.install_fonts()
+      Isabelle_Font.install_fonts()
 
       val init_options = Options.init()
       Swing_Thread.now { PIDE.options.update(init_options)  }
diff -r 81f8da412b7f -r 22d1dd43f089 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Thu Apr 04 17:16:51 2013 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Thu Apr 04 17:33:04 2013 +0200
@@ -30,8 +30,8 @@
 
     font =
       Symbol.fonts.get(symbol) match {
-        case None => Isabelle_System.get_font(size = font_size)
-        case Some(font_family) => Isabelle_System.get_font(family = font_family, size = font_size)
+        case None => Isabelle_Font(size = font_size)
+        case Some(font_family) => Isabelle_Font(family = font_family, size = font_size)
       }
     action =
       Action(decoded) {