diff -r ee4cf96a9406 -r 58aa6749ff36 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Thu Jun 01 21:43:36 2017 +0200 +++ b/src/Pure/Thy/html.scala Thu Jun 01 23:12:48 2017 +0200 @@ -174,6 +174,9 @@ def style(s: String): XML.Elem = XML.elem("style", text(s)) + def style_file(href: String): XML.Elem = + XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil) + /* messages */ @@ -208,29 +211,60 @@ XML.Elem(Markup("meta", List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) - def head_css(css: String): XML.Elem = - XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil) - def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css", hidden: Boolean = true): String = { cat_lines( List(header, output( - XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head), + XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head), hidden = hidden), output(XML.elem("body", body), hidden = hidden))) } + /* fonts */ + + def fonts_url(): String => String = + (for (font <- Isabelle_System.fonts(html = true)) + yield (font.base_name -> Url.print_file(font.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): 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) ::: + List("}")) + + List( + "/* Isabelle fonts */", + font_face("IsabelleText", "IsabelleText.ttf"), + font_face("IsabelleText", "IsabelleTextBold.ttf", bold = true), + font_face("Vacuous", "Vacuous.ttf")).mkString("\n\n") + } + + /* document directory */ def isabelle_css: Path = Path.explode("~~/etc/isabelle.css") + def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts")) + { + File.write(dir + isabelle_css.base, + fonts_css(make_url) + "\n\n\n" + File.read(isabelle_css)) + } + def init_dir(dir: Path) { Isabelle_System.mkdirs(dir) - File.copy(isabelle_css, dir) + write_isabelle_css(dir) } def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,