# 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)