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