tuned output;
authorwenzelm
Thu, 29 Jun 2017 21:07:47 +0200
changeset 66220 68671cc5d40a
parent 66219 f037cdaa5ca0
child 66221 e6b7edd12f05
tuned output;
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)
   }