src/Pure/General/http.scala
changeset 69363 0675481ce575
parent 69360 dc9a39c3f75d
child 69364 91dbade9a5fa
--- a/src/Pure/General/http.scala	Wed Nov 28 14:40:06 2018 +0100
+++ b/src/Pure/General/http.scala	Wed Nov 28 14:51:24 2018 +0100
@@ -154,8 +154,8 @@
 
   /* fonts */
 
-  private lazy val html_fonts: SortedMap[String, Bytes] =
-    SortedMap(Isabelle_Fonts.fonts(html = true).map(entry => (entry.name -> entry.bytes)): _*)
+  private lazy val html_fonts: List[(String, Bytes)] =
+    Isabelle_Fonts.fonts(html = true).map(entry => (entry.name -> entry.bytes))
 
   def fonts(root: String = "/fonts"): Handler =
     get(root, arg =>