# HG changeset patch
# User wenzelm
# Date 1660307977 -7200
# Node ID d06cae2b407a7101519f72a6cba3626d3e5a79b7
# Parent  9f7abd148545df48746afe245f6699fabeafaa37
unused (despite cf52379c0776);

diff -r 9f7abd148545 -r d06cae2b407a src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 12 14:33:50 2022 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 12 14:39:37 2022 +0200
@@ -686,12 +686,6 @@
       state.command_results(version, command)
 
 
-    /* command ids: static and dynamic */
-
-    def command_id_map: Map[Document_ID.Generic, Command] =
-      state.command_id_map(version, get_node(node_name).commands)
-
-
     /* cumulate markup */
 
     def cumulate[A](
@@ -1090,18 +1084,6 @@
         removing_versions = false)
     }
 
-    def command_id_map(
-      version: Version,
-      commands: Iterable[Command]
-    ) : Map[Document_ID.Generic, Command] = {
-      require(is_assigned(version), "version not assigned (command_id_map)")
-      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_maybe_consolidated(version: Version, command: Command): Boolean = {
       require(is_assigned(version), "version not assigned (command_maybe_consolidated)")
       try {