clarified output;
authorwenzelm
Thu, 01 Jun 2017 20:52:31 +0200
changeset 65995 145283346958
parent 65994 46123b9dadc8
child 65996 e72f7291ad6c
clarified output;
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)
   }
 }