# HG changeset patch
# User wenzelm
# Date 1528731464 -7200
# Node ID 21465884037a827710e90ae1ab9bb55fed491472
# Parent  33114721ac9a616a4fa0277b8322d6927edff47c
clarified signature: persistent results;

diff -r 33114721ac9a -r 21465884037a src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Jun 11 15:50:28 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Jun 11 17:37:44 2018 +0200
@@ -539,6 +539,7 @@
     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 exports_map: Map[String, Export.Entry]
 
     def find_command(id: Document_ID.Generic): Option[(Node, Command)]
     def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
@@ -1030,7 +1031,7 @@
         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)] =
+        lazy val messages: List[(XML.Tree, Position.T)] =
           (for {
             (command, start) <-
               Document.Node.Commands.starts_pos(
@@ -1039,13 +1040,16 @@
             (_, tree) <- state.command_results(version, command).iterator
            } yield (tree, pos)).toList
 
-        def exports: List[Export.Entry] =
+        lazy val 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
 
+        lazy val exports_map: Map[String, Export.Entry] =
+          (for (entry <- exports.iterator) yield (entry.name, entry)).toMap
+
 
         /* find command */