src/Pure/Thy/html.scala
changeset 66001 b7cea8146285
parent 66000 58aa6749ff36
child 66006 cec184536dfd
equal deleted inserted replaced
66000:58aa6749ff36 66001:b7cea8146285
   168     XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
   168     XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
   169 
   169 
   170   def image(src: String, alt: String = ""): XML.Elem =
   170   def image(src: String, alt: String = ""): XML.Elem =
   171     XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
   171     XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
   172 
   172 
   173   def source(src: String): XML.Elem = div("source", List(pre(text(src))))
   173   def source(src: String): XML.Elem = pre("source", text(src))
   174 
   174 
   175   def style(s: String): XML.Elem = XML.elem("style", text(s))
   175   def style(s: String): XML.Elem = XML.elem("style", text(s))
   176 
   176 
   177   def style_file(href: String): XML.Elem =
   177   def style_file(href: String): XML.Elem =
   178     XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
   178     XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)