--- 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 */
--- a/src/Tools/VSCode/src/preview_panel.scala Thu Jun 29 11:36:25 2017 +0200
+++ b/src/Tools/VSCode/src/preview_panel.scala Thu Jun 29 11:42:42 2017 +0200
@@ -46,7 +46,7 @@
val label = "Preview " + quote(model.node_name.toString)
val content =
HTML.output_document(
- List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
+ List(HTML.style(HTML.fonts_css()), HTML.style_file(HTML.isabelle_css)),
List(
HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
HTML.source(Present.theory_document(snapshot))),
--- a/src/Tools/VSCode/src/state_panel.scala Thu Jun 29 11:36:25 2017 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala Thu Jun 29 11:42:42 2017 +0200
@@ -65,7 +65,7 @@
val content =
HTML.output_document(
List(HTML.style(HTML.fonts_css()),
- HTML.style_file(Url.print_file(HTML.isabelle_css.file)),
+ HTML.style_file(HTML.isabelle_css),
HTML.script(controls_script)),
List(controls, HTML.source(text)),
css = "")