src/Pure/PIDE/document.scala
changeset 44580 3bc9a215a56d
parent 44543 ba8f24f7156e
child 44581 7daef43592d0
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 30 12:24:55 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 30 15:43:27 2011 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4      val version: Version
     1.5      val node: Node
     1.6      val is_outdated: Boolean
     1.7 -    def lookup_command(id: Command_ID): Option[Command]
     1.8 +    def find_command(id: Command_ID): Option[(String, Node, Command)]
     1.9      def state(command: Command): Command.State
    1.10      def convert(i: Text.Offset): Text.Offset
    1.11      def convert(range: Text.Range): Text.Range
    1.12 @@ -370,7 +370,13 @@
    1.13          val node = version.nodes(name)
    1.14          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    1.15  
    1.16 -        def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
    1.17 +        def find_command(id: Command_ID): Option[(String, Node, Command)] =
    1.18 +          State.this.lookup_command(id) match {
    1.19 +            case None => None
    1.20 +            case Some(command) =>
    1.21 +              version.nodes.find({ case (_, node) => node.commands(command) })
    1.22 +                .map({ case (name, node) => (name, node, command) })
    1.23 +          }
    1.24  
    1.25          def state(command: Command): Command.State =
    1.26            try {