# HG changeset patch
# User wenzelm
# Date 1543414281 -3600
# Node ID 91dbade9a5fafecb2d7343536d6bfb82cd6265f6
# Parent  0675481ce57554df241966bd212fda235a8606e8
proper font file name for HTTP (amending dc9a39c3f75d);
clarified Entry content;

diff -r 0675481ce575 -r 91dbade9a5fa src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Wed Nov 28 14:51:24 2018 +0100
+++ b/src/Pure/General/http.scala	Wed Nov 28 15:11:21 2018 +0100
@@ -154,14 +154,18 @@
 
   /* fonts */
 
-  private lazy val html_fonts: List[(String, Bytes)] =
-    Isabelle_Fonts.fonts(html = true).map(entry => (entry.name -> entry.bytes))
+  private lazy val html_fonts: List[Isabelle_Fonts.Entry] = Isabelle_Fonts.fonts(html = true)
 
   def fonts(root: String = "/fonts"): Handler =
     get(root, arg =>
       {
         val uri_name = arg.uri.toString
-        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) })
+        if (uri_name == root) {
+          Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.base_name))))
+        }
+        else {
+          html_fonts.collectFirst(
+            { case entry if uri_name == root + "/" + entry.path.base_name => Response(entry.bytes) })
+        }
       })
 }
diff -r 0675481ce575 -r 91dbade9a5fa src/Pure/System/isabelle_fonts.scala
--- a/src/Pure/System/isabelle_fonts.scala	Wed Nov 28 14:51:24 2018 +0100
+++ b/src/Pure/System/isabelle_fonts.scala	Wed Nov 28 15:11:21 2018 +0100
@@ -36,9 +36,9 @@
 
   sealed case class Entry(path: Path, html: Boolean = false)
   {
-    def bytes: Bytes = Bytes.read(path)
+    lazy val bytes: Bytes = Bytes.read(path)
+    lazy val font: Font = Font.createFont(Font.TRUETYPE_FONT, path.file)
 
-    lazy val font: Font = Font.createFont(Font.TRUETYPE_FONT, path.file)
     def family: String = font.getFamily
     def name: String = font.getFontName
     def style: Int =