--- 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 */