# HG changeset patch
# User wenzelm
# Date 1488467386 -3600
# Node ID 548efa2bda664b4ba596f54870de8dadac2e2ba9
# Parent  9d53b892140afc7656ee8768632b37f479f035fb
tuned;

diff -r 9d53b892140a -r 548efa2bda66 src/Pure/General/graphics_file.scala
--- 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))
diff -r 9d53b892140a -r 548efa2bda66 src/Pure/General/http.scala
--- 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) })
       })
   }
 }