# HG changeset patch
# User wenzelm
# Date 1488466603 -3600
# Node ID 9a0e34edfad18e21f9e86d4de6d5526aa45fa339
# Parent  2e99c0ee3bacdeade854c1d4928414b08a561a18
tuned;

diff -r 2e99c0ee3bac -r 9a0e34edfad1 src/Pure/Admin/news.scala
--- a/src/Pure/Admin/news.scala	Thu Mar 02 15:46:27 2017 +0100
+++ b/src/Pure/Admin/news.scala	Thu Mar 02 15:56:43 2017 +0100
@@ -22,8 +22,7 @@
       "</pre>\n" +
       HTML.end_document)
 
-    for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
-      File.copy(font, target)
+    for (font <- Isabelle_System.fonts()) File.copy(font, target)
 
     File.copy(Path.explode("~~/etc/isabelle.css"), target)
   }
diff -r 2e99c0ee3bac -r 9a0e34edfad1 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Thu Mar 02 15:46:27 2017 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Mar 02 15:56:43 2017 +0100
@@ -262,7 +262,7 @@
   def install_fonts()
   {
     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
-    for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
+    for (font <- Isabelle_System.fonts())
       ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
   }
 }
diff -r 2e99c0ee3bac -r 9a0e34edfad1 src/Pure/GUI/jfx_gui.scala
--- a/src/Pure/GUI/jfx_gui.scala	Thu Mar 02 15:46:27 2017 +0100
+++ b/src/Pure/GUI/jfx_gui.scala	Thu Mar 02 15:56:43 2017 +0100
@@ -44,7 +44,7 @@
 
   def install_fonts()
   {
-    for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS"))) {
+    for (font <- Isabelle_System.fonts()) {
       val stream = new BufferedInputStream(new FileInputStream(font.file))
       try { JFX_Font.loadFont(stream, 1.0) }
       finally { stream.close }
diff -r 2e99c0ee3bac -r 9a0e34edfad1 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Mar 02 15:46:27 2017 +0100
+++ b/src/Pure/General/http.scala	Thu Mar 02 15:56:43 2017 +0100
@@ -132,10 +132,7 @@
 
   private lazy val isabelle_fonts: SortedMap[String, Bytes] =
     SortedMap(
-      (for {
-        variable <- List("ISABELLE_FONTS", "ISABELLE_FONTS_HTML")
-        path <- Path.split(Isabelle_System.getenv_strict(variable))
-      } yield (path.base.implode -> Bytes.read(path))): _*)
+      Isabelle_System.fonts(html = true).map(path => (path.base.implode -> Bytes.read(path))): _*)
 
   def fonts(root: String = "/fonts"): Handler =
   {
diff -r 2e99c0ee3bac -r 9a0e34edfad1 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Mar 02 15:46:27 2017 +0100
+++ b/src/Pure/System/isabelle_system.scala	Thu Mar 02 15:56:43 2017 +0100
@@ -335,6 +335,19 @@
     Path.split(getenv_strict("ISABELLE_COMPONENTS"))
 
 
+  /* fonts */
+
+  def fonts(html: Boolean = false): List[Path] =
+  {
+    val variables =
+      if (html) List("ISABELLE_FONTS", "ISABELLE_FONTS_HTML") else List("ISABELLE_FONTS")
+    for {
+      variable <- variables
+      path <- Path.split(Isabelle_System.getenv_strict(variable))
+    } yield path
+  }
+
+
   /* default logic */
 
   def default_logic(args: String*): String =
diff -r 2e99c0ee3bac -r 9a0e34edfad1 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Thu Mar 02 15:46:27 2017 +0100
+++ b/src/Pure/Thy/present.scala	Thu Mar 02 15:56:43 2017 +0100
@@ -110,9 +110,7 @@
 
       File.copy(Path.explode("~~/etc/isabelle.css"), session_prefix)
 
-      for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
-        File.copy(font, session_prefix)
-      for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS_HTML")))
+      for (font <- Isabelle_System.fonts(html = true))
         File.copy(font, session_prefix)
     }
   }