--- 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 */
--- 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))
--- 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))
+ }
}
--- 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)
}
--- 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 = "")
}