tuned signature;
authorwenzelm
Fri, 11 Jan 2019 16:36:21 +0100
changeset 69633 3d91a7a58113
parent 69630 aaa0b5f571e8
child 69634 70f1994988d4
tuned signature;
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