diff -r 3b709d9074ec -r dc9a39c3f75d src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Wed Nov 28 13:59:29 2018 +0100 +++ b/src/Pure/Thy/html.scala Wed Nov 28 14:00:22 2018 +0100 @@ -350,40 +350,25 @@ /* fonts */ def fonts_url(): String => String = - (for (path <- Isabelle_Fonts.files(html = true)) - yield (path.base_name -> Url.print_file(path.file))).toMap + (for (entry <- Isabelle_Fonts.fonts(html = true)) + yield (entry.name -> Url.print_file(entry.path.file))).toMap def fonts_dir(prefix: String)(ttf_name: String): String = prefix + "/" + ttf_name def fonts_css(make_url: String => String = fonts_url()): String = { - def font_face( - name: String, ttf_name: String, bold: Boolean = false, italic: Boolean = false): String = + def font_face(entry: Isabelle_Fonts.Entry): String = cat_lines( List( "@font-face {", - " font-family: '" + name + "';", - " src: url('" + make_url(ttf_name) + "') format('truetype');") ::: - (if (bold) List(" font-weight: bold;") else Nil) ::: - (if (italic) List(" font-style: italic;") else Nil) ::: + " font-family: '" + entry.family + "';", + " src: url('" + make_url(entry.path.base_name) + "') format('truetype');") ::: + (if (entry.is_bold) List(" font-weight: bold;") else Nil) ::: + (if (entry.is_italic) List(" font-style: italic;") else Nil) ::: List("}")) - List( - "/* Isabelle fonts */", - font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono.ttf"), - font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-Bold.ttf", bold = true), - font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-Oblique.ttf", italic = true), - font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-BoldOblique.ttf", bold = true, italic = true), - font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans.ttf"), - font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-Bold.ttf", bold = true), - font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-Oblique.ttf", italic = true), - font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-BoldOblique.ttf", bold = true, italic = true), - font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif.ttf"), - font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-Bold.ttf", bold = true), - font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-Italic.ttf", italic = true), - font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-BoldItalic.ttf", bold = true, italic = true), - font_face("Vacuous", "Vacuous.ttf")).mkString("\n\n") + ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(html = true).map(font_face(_))).mkString("\n\n") }