# HG changeset patch
# User wenzelm
# Date 1543400882 -3600
# Node ID cdc2de88d6576b507a1b4e927ac6eb4d295ddf5a
# Parent  600727ff6889d7ba32eec7c83db959ecc05c20cf
clarified modules;

diff -r 600727ff6889 -r cdc2de88d657 src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Wed Nov 28 11:06:58 2018 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Wed Nov 28 11:28:02 2018 +0100
@@ -62,7 +62,7 @@
   val etc_preferences: Path = etc + Path.explode("preferences")
 
   def fonts(html: Boolean = false): List[Path] =
-    Isabelle_System.fonts(html = html, get = getenv(_))
+    Isabelle_Fonts.files(html = html, getenv = getenv(_))
 
 
   /* settings */
diff -r 600727ff6889 -r cdc2de88d657 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Wed Nov 28 11:06:58 2018 +0100
+++ b/src/Pure/GUI/gui.scala	Wed Nov 28 11:28:02 2018 +0100
@@ -242,8 +242,8 @@
   def install_fonts()
   {
     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
-    for (font <- Isabelle_System.fonts())
-      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
+    for (path <- Isabelle_Fonts.files())
+      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, path.file))
   }
 }
 
diff -r 600727ff6889 -r cdc2de88d657 src/Pure/General/graphics_file.scala
--- a/src/Pure/General/graphics_file.scala	Wed Nov 28 11:06:58 2018 +0100
+++ b/src/Pure/General/graphics_file.scala	Wed Nov 28 11:28:02 2018 +0100
@@ -45,7 +45,7 @@
   {
     val mapper = new DefaultFontMapper
     for {
-      font <- Isabelle_System.fonts()
+      font <- Isabelle_Fonts.files()
       name <- Library.try_unsuffix(".ttf", font.base_name)
     } {
       val parameters = new DefaultFontMapper.BaseFontParameters(File.platform_path(font))
diff -r 600727ff6889 -r cdc2de88d657 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Wed Nov 28 11:06:58 2018 +0100
+++ b/src/Pure/General/http.scala	Wed Nov 28 11:28:02 2018 +0100
@@ -156,7 +156,7 @@
 
   private lazy val html_fonts: SortedMap[String, Bytes] =
     SortedMap(
-      Isabelle_System.fonts(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
+      Isabelle_Fonts.files(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
 
   def fonts(root: String = "/fonts"): Handler =
     get(root, arg =>
diff -r 600727ff6889 -r cdc2de88d657 src/Pure/System/isabelle_fonts.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_fonts.scala	Wed Nov 28 11:28:02 2018 +0100
@@ -0,0 +1,27 @@
+/*  Title:      Pure/System/isabelle_system.scala
+    Author:     Makarius
+
+Fonts from the Isabelle system environment, notably the "Isabelle DejaVu"
+collection.
+*/
+
+package isabelle
+
+
+object Isabelle_Fonts
+{
+  /* Isabelle system environment */
+
+  def variables(html: Boolean = false): List[String] =
+    if (html) List("ISABELLE_FONTS", "ISABELLE_FONTS_HTML") else List("ISABELLE_FONTS")
+
+  def files(
+    html: Boolean = false,
+    getenv: String => String = Isabelle_System.getenv_strict(_)): List[Path] =
+  {
+    for {
+      variable <- variables(html = html)
+      path <- Path.split(getenv(variable))
+    } yield path
+  }
+}
diff -r 600727ff6889 -r cdc2de88d657 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Nov 28 11:06:58 2018 +0100
+++ b/src/Pure/System/isabelle_system.scala	Wed Nov 28 11:28:02 2018 +0100
@@ -365,19 +365,6 @@
   }
 
 
-  /* fonts */
-
-  def fonts(html: Boolean = false, get: String => String = getenv_strict(_)): List[Path] =
-  {
-    val variables =
-      if (html) List("ISABELLE_FONTS", "ISABELLE_FONTS_HTML") else List("ISABELLE_FONTS")
-    for {
-      variable <- variables
-      path <- Path.split(get(variable))
-    } yield path
-  }
-
-
   /* default logic */
 
   def default_logic(args: String*): String =
diff -r 600727ff6889 -r cdc2de88d657 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Wed Nov 28 11:06:58 2018 +0100
+++ b/src/Pure/Thy/html.scala	Wed Nov 28 11:28:02 2018 +0100
@@ -350,8 +350,8 @@
   /* fonts */
 
   def fonts_url(): String => String =
-    (for (font <- Isabelle_System.fonts(html = true))
-     yield (font.base_name -> Url.print_file(font.file))).toMap
+    (for (path <- Isabelle_Fonts.files(html = true))
+     yield (path.base_name -> Url.print_file(path.file))).toMap
 
   def fonts_dir(prefix: String)(ttf_name: String): String =
     prefix + "/" + ttf_name
diff -r 600727ff6889 -r cdc2de88d657 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Wed Nov 28 11:06:58 2018 +0100
+++ b/src/Pure/Thy/present.scala	Wed Nov 28 11:28:02 2018 +0100
@@ -96,8 +96,8 @@
 
       HTML.write_isabelle_css(session_prefix)
 
-      for (font <- Isabelle_System.fonts(html = true))
-        File.copy(font, session_fonts)
+      for (path <- Isabelle_Fonts.files(html = true))
+        File.copy(path, session_fonts)
     }
   }
 
diff -r 600727ff6889 -r cdc2de88d657 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Nov 28 11:06:58 2018 +0100
+++ b/src/Pure/build-jars	Wed Nov 28 11:28:02 2018 +0100
@@ -118,6 +118,7 @@
   System/getopts.scala
   System/invoke_scala.scala
   System/isabelle_charset.scala
+  System/isabelle_fonts.scala
   System/isabelle_process.scala
   System/isabelle_system.scala
   System/isabelle_tool.scala