diff -r 77c93eaf6cb7 -r 0675481ce575 src/Pure/General/http.scala --- 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 =>