src/Pure/PIDE/document.scala
changeset 44581 7daef43592d0
parent 44580 3bc9a215a56d
child 44582 479c07072992
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 30 15:43:27 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 30 15:49:27 2011 +0200
     1.3 @@ -270,6 +270,7 @@
     1.4      }
     1.5  
     1.6      def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
     1.7 +    def lookup_exec(id: Exec_ID): Option[Command] = execs.get(id).map(_.command)
     1.8  
     1.9      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
    1.10      def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)  // FIXME rename
    1.11 @@ -370,8 +371,8 @@
    1.12          val node = version.nodes(name)
    1.13          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    1.14  
    1.15 -        def find_command(id: Command_ID): Option[(String, Node, Command)] =
    1.16 -          State.this.lookup_command(id) match {
    1.17 +        def find_command(id: ID): Option[(String, Node, Command)] =
    1.18 +          State.this.lookup_command(id) orElse State.this.lookup_exec(id) match {
    1.19              case None => None
    1.20              case Some(command) =>
    1.21                version.nodes.find({ case (_, node) => node.commands(command) })