# HG changeset patch
# User wenzelm
# Date 1547220981 -3600
# Node ID 3d91a7a581130f589b43a14cf71b8669b2782a00
# Parent  aaa0b5f571e83044fdeaf39880e46cf5c79c939d
tuned signature;

diff -r aaa0b5f571e8 -r 3d91a7a58113 src/Pure/PIDE/document.scala
--- 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