src/Pure/PIDE/document.scala
changeset 44607 274eff0ea12e
parent 44582 479c07072992
child 44613 a3255c85327b
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Aug 31 14:39:41 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 31 15:41:22 2011 +0200
     1.3 @@ -271,13 +271,12 @@
     1.4  
     1.5      def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
     1.6  
     1.7 -    def find_command(version: Version, id: ID): Option[(String, Node, Command)] =
     1.8 +    def find_command(version: Version, id: ID): Option[(Node, Command)] =
     1.9        commands.get(id) orElse execs.get(id) match {
    1.10          case None => None
    1.11          case Some(st) =>
    1.12            val command = st.command
    1.13 -          version.nodes.find({ case (_, node) => node.commands(command) })
    1.14 -            .map({ case (name, node) => (name, node, command) })
    1.15 +          version.nodes.get(command.node_name).map((_, command))
    1.16        }
    1.17  
    1.18      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)