--- a/src/Pure/Thy/thy_resources.scala Tue May 29 15:04:02 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala Tue May 29 17:45:48 2018 +0200
@@ -60,6 +60,7 @@
val version: Document.Version,
val nodes: List[(Document.Node.Name, Protocol.Node_Status)])
{
+ def node_names: List[Document.Node.Name] = nodes.map(_._1)
def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
def messages(node_name: Document.Node.Name): List[(XML.Tree, Position.T)] =
@@ -73,6 +74,13 @@
} yield (tree, pos)).toList
}
+ def markup_to_XML(node_name: Document.Node.Name,
+ range: Text.Range = Text.Range.full,
+ elements: Markup.Elements = Markup.Elements.full): XML.Body =
+ {
+ state.markup_to_XML(version, node_name, range, elements)
+ }
+
def exports(node_name: Document.Node.Name): List[Export.Entry] =
{
val node = version.nodes(node_name)