src/Pure/Thy/thy_resources.scala

   sealed case class Theories_Result(
     val state: Document.State,
     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)] =
     {
       val node = version.nodes(node_name)

         (command, start) <-
           Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node))
         pos = command.span.keyword_pos(start).position(command.span.name)
         (_, tree) <- state.command_results(version, command).iterator
        } 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)