systematic access to command ids;
authorwenzelm
Tue Aug 28 21:08:05 2018 +0200 (13 months ago)
changeset 68836cf52379c0776
parent 68835 2e59da922630
child 68837 99f0aee4adbd
systematic access to command ids;
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 28 15:25:28 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 28 21:08:05 2018 +0200
     1.3 @@ -560,6 +560,8 @@
     1.4  
     1.5      def command_results(range: Text.Range): Command.Results
     1.6      def command_results(command: Command): Command.Results
     1.7 +
     1.8 +    def command_id_map: Map[Document_ID.Generic, Command]
     1.9    }
    1.10  
    1.11  
    1.12 @@ -860,6 +862,17 @@
    1.13          removing_versions = false)
    1.14      }
    1.15  
    1.16 +    def command_id_map(version: Version, commands: Iterable[Command])
    1.17 +      : Map[Document_ID.Generic, Command] =
    1.18 +    {
    1.19 +      require(is_assigned(version))
    1.20 +      val assignment = the_assignment(version).check_finished
    1.21 +      (for {
    1.22 +        command <- commands.iterator
    1.23 +        id <- (command.id :: assignment.command_execs.getOrElse(command.id, Nil)).iterator
    1.24 +      } yield (id -> command)).toMap
    1.25 +    }
    1.26 +
    1.27      def command_state_eval(version: Version, command: Command): Option[Command.State] =
    1.28      {
    1.29        require(is_assigned(version))
    1.30 @@ -1148,6 +1161,12 @@
    1.31            state.command_results(version, command)
    1.32  
    1.33  
    1.34 +        /* command ids: static and dynamic */
    1.35 +
    1.36 +        def command_id_map: Map[Document_ID.Generic, Command] =
    1.37 +          state.command_id_map(version, version.nodes(node_name).commands)
    1.38 +
    1.39 +
    1.40          /* output */
    1.41  
    1.42          override def toString: String =