--- a/src/Pure/General/graphics_file.scala Thu Mar 02 16:05:09 2017 +0100
+++ b/src/Pure/General/graphics_file.scala Thu Mar 02 16:09:46 2017 +0100
@@ -45,7 +45,7 @@
{
val mapper = new DefaultFontMapper
for {
- font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS"))
+ font <- Isabelle_System.fonts()
name <- Library.try_unsuffix(".ttf", font.base.implode)
} {
val parameters = new DefaultFontMapper.BaseFontParameters(File.platform_path(font))
--- a/src/Pure/General/http.scala Thu Mar 02 16:05:09 2017 +0100
+++ b/src/Pure/General/http.scala Thu Mar 02 16:09:46 2017 +0100
@@ -130,7 +130,7 @@
/* fonts */
- private lazy val isabelle_fonts: SortedMap[String, Bytes] =
+ private lazy val html_fonts: SortedMap[String, Bytes] =
SortedMap(
Isabelle_System.fonts(html = true).map(path => (path.base.implode -> Bytes.read(path))): _*)
@@ -139,10 +139,8 @@
get(root, uri =>
{
val uri_name = uri.toString
- if (uri_name == root) Some(Response.text(cat_lines(isabelle_fonts.map(_._1))))
- else
- isabelle_fonts.collectFirst(
- { case (name, file) if uri_name == root + "/" + name => Response(file) })
+ if (uri_name == root) Some(Response.text(cat_lines(html_fonts.map(_._1))))
+ else html_fonts.collectFirst({ case (a, b) if uri_name == root + "/" + a => Response(b) })
})
}
}