# HG changeset patch
# User wenzelm
# Date 1535483285 -7200
# Node ID cf52379c0776c600909adb32d7a9689db9bc5b5a
# Parent  2e59da92263029ddc4f184ab2c6868d84143f5fa
systematic access to command ids;

diff -r 2e59da922630 -r cf52379c0776 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 28 15:25:28 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 28 21:08:05 2018 +0200
@@ -560,6 +560,8 @@
 
     def command_results(range: Text.Range): Command.Results
     def command_results(command: Command): Command.Results
+
+    def command_id_map: Map[Document_ID.Generic, Command]
   }
 
 
@@ -860,6 +862,17 @@
         removing_versions = false)
     }
 
+    def command_id_map(version: Version, commands: Iterable[Command])
+      : Map[Document_ID.Generic, Command] =
+    {
+      require(is_assigned(version))
+      val assignment = the_assignment(version).check_finished
+      (for {
+        command <- commands.iterator
+        id <- (command.id :: assignment.command_execs.getOrElse(command.id, Nil)).iterator
+      } yield (id -> command)).toMap
+    }
+
     def command_state_eval(version: Version, command: Command): Option[Command.State] =
     {
       require(is_assigned(version))
@@ -1148,6 +1161,12 @@
           state.command_results(version, command)
 
 
+        /* command ids: static and dynamic */
+
+        def command_id_map: Map[Document_ID.Generic, Command] =
+          state.command_id_map(version, version.nodes(node_name).commands)
+
+
         /* output */
 
         override def toString: String =