diff -r 5c579bb9adb1 -r f9379279f98c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Jun 03 19:06:56 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Jun 03 20:37:16 2018 +0200
@@ -537,6 +537,8 @@
     def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
 
     def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
+    def messages: List[(XML.Tree, Position.T)]
+    def exports: List[Export.Entry]
 
     def find_command(id: Document_ID.Generic): Option[(Node, Command)]
     def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
@@ -1006,6 +1008,22 @@
         def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
           state.markup_to_XML(version, node_name, range, elements)
 
+        def messages: List[(XML.Tree, Position.T)] =
+          (for {
+            (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 exports: List[Export.Entry] =
+          Command.Exports.merge(
+            for {
+              command <- node.commands.iterator
+              st <- state.command_states(version, command).iterator
+            } yield st.exports).iterator.map(_._2).toList
+
 
         /* find command */