src/Pure/General/html.scala
changeset 80203 ca9a402735b4
parent 80018 ac4412562c7b
child 80429 6f4d5d922da7
equal deleted inserted replaced
80202:03c058592c58 80203:ca9a402735b4
    91   def style(s: String): XML.Elem = XML.elem("style", text(s))
    91   def style(s: String): XML.Elem = XML.elem("style", text(s))
    92   def style_file(href: String): XML.Elem =
    92   def style_file(href: String): XML.Elem =
    93     XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
    93     XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
    94   def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file))
    94   def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file))
    95 
    95 
    96   def script(s: String): XML.Elem = XML.elem("script", text(s))
    96   def script(s: String): XML.Elem = XML.elem("script", List(raw(text(s))))
    97   def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil)
    97   def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil)
    98   def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
    98   def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
    99 
    99 
   100 
   100 
   101   /* href */
   101   /* href */