src/Pure/Thy/html.scala
changeset 66040 f826ba18fe08
parent 66018 9ce3720976dc
child 66196 31c9b09cc1d4
equal deleted inserted replaced
66039:a2b8c3d31037 66040:f826ba18fe08
   191     XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
   191     XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
   192 
   192 
   193   def image(src: String, alt: String = ""): XML.Elem =
   193   def image(src: String, alt: String = ""): XML.Elem =
   194     XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
   194     XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
   195 
   195 
   196   def source(src: String): XML.Elem = pre("source", text(src))
   196   def source(body: XML.Body): XML.Elem = pre("source", body)
       
   197   def source(src: String): XML.Elem = source(text(src))
   197 
   198 
   198   def style(s: String): XML.Elem = XML.elem("style", text(s))
   199   def style(s: String): XML.Elem = XML.elem("style", text(s))
   199 
   200 
   200   def style_file(href: String): XML.Elem =
   201   def style_file(href: String): XML.Elem =
   201     XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
   202     XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)