# HG changeset patch
# User wenzelm
# Date 1498763267 -7200
# Node ID 68671cc5d40ab77f2bc482cd997dbb99bcfdcc1d
# Parent  f037cdaa5ca0cb84bb88c3bee2520f7efcfef27b
tuned output;

diff -r f037cdaa5ca0 -r 68671cc5d40a src/Tools/VSCode/src/preview_panel.scala
--- 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)
   }