# HG changeset patch
# User wenzelm
# Date 1496923687 -7200
# Node ID f826ba18fe08aec707358981c565ec2d6e262f48
# Parent  a2b8c3d310372e0483bb80ce3e39511068b4891a
HTML preview based on PIDE markup;

diff -r a2b8c3d31037 -r f826ba18fe08 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Jun 08 13:17:40 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Jun 08 14:08:07 2017 +0200
@@ -452,10 +452,13 @@
 
     def node_name: Node.Name
     def node: Node
+
     def commands_loading: List[Command]
     def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
     def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
 
+    def markup_to_XML(elements: Markup.Elements): XML.Body
+
     def find_command(id: Document_ID.Generic): Option[(Node, Command)]
     def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
       : Option[Line.Node_Position]
@@ -845,6 +848,9 @@
           }
           else version.nodes.commands_loading(other_node_name).headOption
 
+        def markup_to_XML(elements: Markup.Elements): XML.Body =
+          state.markup_to_XML(version, node, elements)
+
 
         /* find command */
 
diff -r a2b8c3d31037 -r f826ba18fe08 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Thu Jun 08 13:17:40 2017 +0200
+++ b/src/Pure/Thy/html.scala	Thu Jun 08 14:08:07 2017 +0200
@@ -193,7 +193,8 @@
   def image(src: String, alt: String = ""): XML.Elem =
     XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
 
-  def source(src: String): XML.Elem = pre("source", text(src))
+  def source(body: XML.Body): XML.Elem = pre("source", body)
+  def source(src: String): XML.Elem = source(text(src))
 
   def style(s: String): XML.Elem = XML.elem("style", text(s))
 
diff -r a2b8c3d31037 -r f826ba18fe08 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Thu Jun 08 13:17:40 2017 +0200
+++ b/src/Pure/Thy/present.scala	Thu Jun 08 14:08:07 2017 +0200
@@ -99,4 +99,30 @@
         File.copy(font, session_fonts)
     }
   }
+
+
+  /* theory document */
+
+  private val document_span_elements =
+    Markup.Elements(Markup.TFREE, Markup.TVAR, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
+      Markup.NUMERAL, Markup.LITERAL, Markup.DELIMITER, Markup.INNER_STRING, Markup.INNER_CARTOUCHE,
+      Markup.INNER_COMMENT, Markup.COMMAND, Markup.KEYWORD1, Markup.KEYWORD2, Markup.KEYWORD3,
+      Markup.QUASI_KEYWORD, Markup.IMPROPER, Markup.OPERATOR, Markup.STRING, Markup.ALT_STRING,
+      Markup.VERBATIM, Markup.CARTOUCHE, Markup.COMMENT)
+
+  def make_html(xml: XML.Body): XML.Body =
+    xml map {
+      case XML.Wrapped_Elem(markup, body1, body2) =>
+        XML.Wrapped_Elem(markup, make_html(body1), make_html(body2))
+      case XML.Elem(markup, body) =>
+        if (document_span_elements(markup.name)) HTML.span(markup.name, make_html(body))
+        else XML.Elem(markup, make_html(body))
+      case XML.Text(text) =>
+        XML.Text(Symbol.decode(text))
+    }
+
+  def theory_document(snapshot: Document.Snapshot): XML.Body =
+  {
+    make_html(snapshot.markup_to_XML(document_span_elements))
+  }
 }
diff -r a2b8c3d31037 -r f826ba18fe08 src/Tools/VSCode/src/preview.scala
--- a/src/Tools/VSCode/src/preview.scala	Thu Jun 08 13:17:40 2017 +0200
+++ b/src/Tools/VSCode/src/preview.scala	Thu Jun 08 14:08:07 2017 +0200
@@ -49,7 +49,7 @@
         List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
         List(
           HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
-          HTML.source(Symbol.decode(snapshot.node.commands.iterator.map(_.source).mkString))),
+          HTML.source(Present.theory_document(snapshot))),
         css = "")
     (label, content)
   }
diff -r a2b8c3d31037 -r f826ba18fe08 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Jun 08 13:17:40 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Jun 08 14:08:07 2017 +0200
@@ -311,7 +311,7 @@
       List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css))),
       List(
         HTML.chapter("Theory " + quote(node_name.theory_base_name)),
-        HTML.source(snapshot.node.commands.iterator.map(_.source).mkString)),
+        HTML.source(Present.theory_document(snapshot))),
       css = "")
   }