# HG changeset patch
# User wenzelm
# Date 1496343151 -7200
# Node ID 1452833469589197c092753b71aad518c962ca25
# Parent  46123b9dadc8d37704d3fc8ef9a1962e196e2ac7
clarified output;

diff -r 46123b9dadc8 -r 145283346958 src/Tools/VSCode/src/preview.scala
--- a/src/Tools/VSCode/src/preview.scala	Thu Jun 01 17:36:29 2017 +0200
+++ b/src/Tools/VSCode/src/preview.scala	Thu Jun 01 20:52:31 2017 +0200
@@ -47,12 +47,8 @@
     val content =
       HTML.output_document(head = Nil, css = "", body =
         List(
-          HTML.chapter(label),
-          HTML.itemize(
-            snapshot.node.commands.toList.flatMap(
-              command =>
-                if (command.span.name == "") None
-                else Some(HTML.text(command.span.name))))))
+          HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
+          HTML.source(Symbol.decode(snapshot.node.commands.iterator.map(_.source).mkString))))
     (label, content)
   }
 }