src/Pure/PIDE/document.scala

 
     val node_name: Node.Name
     val node: Node
     val load_commands: List[Command]
     def is_loaded: Boolean
+
+    def find_command(id: Document_ID.Generic): Option[(Node, Command)]
+    def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
+      : Option[Line.Node_Position]
 
     def cumulate[A](
       range: Text.Range,
       info: A,
       elements: Markup.Elements,

       copy(commands = commands + (id -> command.init_state))
     }
 
     def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
 
-    def find_command(version: Version, id: Document_ID.Generic): Option[(Node, Command)] =
-      commands.get(id) orElse execs.get(id) match {
-        case None => None
-        case Some(st) =>
-          val command = st.command
-          val node = version.nodes(command.node_name)
-          if (node.commands.contains(command)) Some((node, command)) else None
-      }
-
     def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
     def the_static_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
     def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
     def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
 

         val load_commands: List[Command] =
           if (node_name.is_theory) Nil
           else version.nodes.load_commands(node_name)
 
         val is_loaded: Boolean = node_name.is_theory || load_commands.nonEmpty
+
+
+        /* find command */
+
+        def find_command(id: Document_ID.Generic): Option[(Node, Command)] =
+          state.commands.get(id) orElse state.execs.get(id) match {
+            case None => None
+            case Some(st) =>
+              val command = st.command
+              val node = version.nodes(command.node_name)
+              if (node.commands.contains(command)) Some((node, command)) else None
+          }
+
+        def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
+            : Option[Line.Node_Position] =
+          for ((node, command) <- find_command(id))
+          yield {
+            val name = command.node_name.node
+            val sources_iterator =
+              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
+                (if (offset == 0) Iterator.empty
+                 else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
+            val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
+            Line.Node_Position(name, pos)
+          }
 
 
         /* cumulate markup */
 
         def cumulate[A](

             (if (is_outdated) ", outdated" else "") + ")"
       }
     }
   }
 }
-