# HG changeset patch # User wenzelm # Date 1610376231 -3600 # Node ID ff9cd62d2d2093404cbdc9236cc2adcdbefc9863 # Parent b15fe413b4d247066fe454dbdd33a318649782d7 proper ; diff -r b15fe413b4d2 -r ff9cd62d2d20 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Sun Jan 10 22:17:11 2021 +0100 +++ b/src/Pure/Thy/html.scala Mon Jan 11 15:43:51 2021 +0100 @@ -330,6 +330,8 @@ """ """ + val footer: String = """""" + val head_meta: XML.Elem = XML.Elem(Markup("meta", List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) @@ -340,12 +342,14 @@ structural: Boolean = true): String = { cat_lines( - List(header, + List( + header, output( XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head), hidden = hidden, structural = structural), output(XML.elem("body", body), - hidden = hidden, structural = structural))) + hidden = hidden, structural = structural), + footer)) }