--- 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 {