src/Pure/PIDE/document.scala
changeset 68417 21465884037a
parent 68381 2fd3a6d6ba2e
child 68496 7266fb64de69
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Jun 11 15:50:28 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Jun 11 17:37:44 2018 +0200
     1.3 @@ -539,6 +539,7 @@
     1.4      def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
     1.5      def messages: List[(XML.Tree, Position.T)]
     1.6      def exports: List[Export.Entry]
     1.7 +    def exports_map: Map[String, Export.Entry]
     1.8  
     1.9      def find_command(id: Document_ID.Generic): Option[(Node, Command)]
    1.10      def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
    1.11 @@ -1030,7 +1031,7 @@
    1.12          def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
    1.13            state.markup_to_XML(version, node_name, range, elements)
    1.14  
    1.15 -        def messages: List[(XML.Tree, Position.T)] =
    1.16 +        lazy val messages: List[(XML.Tree, Position.T)] =
    1.17            (for {
    1.18              (command, start) <-
    1.19                Document.Node.Commands.starts_pos(
    1.20 @@ -1039,13 +1040,16 @@
    1.21              (_, tree) <- state.command_results(version, command).iterator
    1.22             } yield (tree, pos)).toList
    1.23  
    1.24 -        def exports: List[Export.Entry] =
    1.25 +        lazy val exports: List[Export.Entry] =
    1.26            Command.Exports.merge(
    1.27              for {
    1.28                command <- node.commands.iterator
    1.29                st <- state.command_states(version, command).iterator
    1.30              } yield st.exports).iterator.map(_._2).toList
    1.31  
    1.32 +        lazy val exports_map: Map[String, Export.Entry] =
    1.33 +          (for (entry <- exports.iterator) yield (entry.name, entry)).toMap
    1.34 +
    1.35  
    1.36          /* find command */
    1.37