author | wenzelm |
Thu, 01 Jun 2017 23:17:11 +0200 | |
changeset 66001 | b7cea8146285 |
parent 66000 | 58aa6749ff36 |
child 66002 | c85f677cfb0a |
--- a/src/Pure/Thy/html.scala Thu Jun 01 23:12:48 2017 +0200 +++ b/src/Pure/Thy/html.scala Thu Jun 01 23:17:11 2017 +0200 @@ -170,7 +170,7 @@ 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 = div("source", List(pre(text(src)))) + def source(src: String): XML.Elem = pre("source", text(src)) def style(s: String): XML.Elem = XML.elem("style", text(s))