--- 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)
}
--- 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))
}
}
--- 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 }
--- 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 =
{
--- 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 =
--- 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)
}
}