src/Pure/PIDE/document.scala
changeset 69633 3d91a7a58113
parent 69556 0a38f23ca4c5
child 70284 3e17c3a5fd39
--- a/src/Pure/PIDE/document.scala	Fri Jan 11 11:35:16 2019 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Jan 11 16:36:21 2019 +0100
@@ -761,6 +761,13 @@
       }
     }
 
+    def node_exports(version: Version, node_name: Node.Name): Command.Exports =
+      Command.Exports.merge(
+        for {
+          command <- version.nodes(node_name).commands.iterator
+          st <- command_states(version, command).iterator
+        } yield st.exports)
+
     def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
     {
       val version = the_version(id)
@@ -1071,11 +1078,7 @@
            } yield (tree, pos)).toList
 
         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
+          state.node_exports(version, node_name).iterator.map(_._2).toList
 
         lazy val exports_map: Map[String, Export.Entry] =
           (for (entry <- exports.iterator) yield (entry.name, entry)).toMap