src/Pure/Thy/html.scala

--- a/src/Pure/Thy/html.scala	Thu Jun 29 11:36:25 2017 +0200
+++ b/src/Pure/Thy/html.scala	Thu Jun 29 11:42:42 2017 +0200
@@ -199,9 +199,12 @@
   def style(s: String): XML.Elem = XML.elem("style", text(s))
   def style_file(href: String): XML.Elem =
     XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
+  def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file))
 
   def script(s: String): XML.Elem = XML.elem("script", text(s))
   def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil)
+  def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
+
 
   /* messages */