# HG changeset patch # User wenzelm # Date 1498729362 -7200 # Node ID f41396c15bb1727e0c287566c7c343e255cd996d # Parent 100c9c997e2b3bc87bbe152847271675e07ead1d tuned signature; diff -r 100c9c997e2b -r f41396c15bb1 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 */ diff -r 100c9c997e2b -r f41396c15bb1 src/Tools/VSCode/src/preview_panel.scala --- 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))), diff -r 100c9c997e2b -r f41396c15bb1 src/Tools/VSCode/src/state_panel.scala --- 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 = "")