# HG changeset patch
# User wenzelm
# Date 1314712167 -7200
# Node ID 7daef43592d02271c61915d16829be17a947a308
# Parent  3bc9a215a56d3efce497f245722d63cc02963b03
dynamic exec state lookup for implicit position information (e.g. 'definition' without binding);

diff -r 3bc9a215a56d -r 7daef43592d0 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 30 15:43:27 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 30 15:49:27 2011 +0200
@@ -270,6 +270,7 @@
     }
 
     def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
+    def lookup_exec(id: Exec_ID): Option[Command] = execs.get(id).map(_.command)
 
     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
     def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)  // FIXME rename
@@ -370,8 +371,8 @@
         val node = version.nodes(name)
         val is_outdated = !(pending_edits.isEmpty && latest == stable)
 
-        def find_command(id: Command_ID): Option[(String, Node, Command)] =
-          State.this.lookup_command(id) match {
+        def find_command(id: ID): Option[(String, Node, Command)] =
+          State.this.lookup_command(id) orElse State.this.lookup_exec(id) match {
             case None => None
             case Some(command) =>
               version.nodes.find({ case (_, node) => node.commands(command) })