--- a/src/Tools/VSCode/src/preview_panel.scala Thu Jun 29 20:59:49 2017 +0200
+++ b/src/Tools/VSCode/src/preview_panel.scala Thu Jun 29 21:07:47 2017 +0200
@@ -43,13 +43,11 @@
def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
{
- val label = "Preview " + quote(model.node_name.toString)
+ val label = "Preview " + quote(model.node_name.theory_base_name)
val content =
HTML.output_document(
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))),
+ List(HTML.source(Present.theory_document(snapshot))),
css = "")
(label, content)
}