diff -r a2b8c3d31037 -r f826ba18fe08 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Thu Jun 08 13:17:40 2017 +0200 +++ b/src/Pure/Thy/html.scala Thu Jun 08 14:08:07 2017 +0200 @@ -193,7 +193,8 @@ def image(src: String, alt: String = ""): XML.Elem = XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) - def source(src: String): XML.Elem = pre("source", text(src)) + def source(body: XML.Body): XML.Elem = pre("source", body) + def source(src: String): XML.Elem = source(text(src)) def style(s: String): XML.Elem = XML.elem("style", text(s))