# HG changeset patch
# User wenzelm
# Date 1543413084 -3600
# Node ID 0675481ce57554df241966bd212fda235a8606e8
# Parent  77c93eaf6cb75db35b4361e52610e57c0539baba
clarified order;

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 =>
diff -r 77c93eaf6cb7 -r 0675481ce575 src/Pure/System/isabelle_fonts.scala
--- a/src/Pure/System/isabelle_fonts.scala	Wed Nov 28 14:40:06 2018 +0100
+++ b/src/Pure/System/isabelle_fonts.scala	Wed Nov 28 14:51:24 2018 +0100
@@ -22,6 +22,18 @@
 
   /* environment entries */
 
+  object Entry
+  {
+    object Ordering extends scala.math.Ordering[Entry]
+    {
+      def compare(entry1: Entry, entry2: Entry): Int =
+        entry1.family compare entry2.family match {
+          case 0 => entry1.style compare entry2.style
+          case ord => ord
+        }
+    }
+  }
+
   sealed case class Entry(path: Path, html: Boolean = false)
   {
     def bytes: Bytes = Bytes.read(path)
@@ -29,13 +41,17 @@
     lazy val font: Font = Font.createFont(Font.TRUETYPE_FONT, path.file)
     def family: String = font.getFamily
     def name: String = font.getFontName
+    def style: Int =
+      (if (is_bold) Font.BOLD else 0) +
+      (if (is_italic) Font.ITALIC else 0)
 
-    // educated guessing
+    // educated guess for style: Font.createFont always produces Font.PLAIN
     private lazy val name_lowercase = Word.lowercase(name)
     def is_bold: Boolean =
       name_lowercase.containsSlice("bold")
     def is_italic: Boolean =
-      name_lowercase.containsSlice("italic") || name_lowercase.containsSlice("oblique")
+      name_lowercase.containsSlice("italic") ||
+      name_lowercase.containsSlice("oblique")
   }
 
   def make_entries(
@@ -46,7 +62,8 @@
     (if (html) Path.split(getenv("ISABELLE_FONTS_HTML")).map(Entry(_, html = true)) else Nil)
   }
 
-  private lazy val all_fonts: List[Entry] = make_entries(html = true)
+  private lazy val all_fonts: List[Entry] =
+    make_entries(html = true).sorted(Entry.Ordering)
 
   def fonts(html: Boolean = false): List[Entry] =
     if (html) all_fonts else all_fonts.filter(entry => !entry.html)