# HG changeset patch
# User wenzelm
# Date 1535642683 -7200
# Node ID b888de4fe58ca7b2f3b5a7aac9d76cc63a34e029
# Parent  e5097a5b2e58d5dc3edc8dd373ba8889388557e3
clarified signature;

diff -r e5097a5b2e58 -r b888de4fe58c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Aug 30 14:56:04 2018 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 30 17:24:43 2018 +0200
@@ -706,14 +706,16 @@
     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)
 
+    def lookup_id(id: Document_ID.Generic): Option[Command.State] =
+      commands.get(id) orElse execs.get(id)
+
     private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean =
       id == st.command.id ||
       (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
 
     private def other_id(id: Document_ID.Generic)
       : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] =
-      (execs.get(id) orElse commands.get(id)).map(st =>
-        ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)))
+      lookup_id(id).map(st => ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)))
 
     private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
       (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
@@ -1077,7 +1079,7 @@
         /* find command */
 
         def find_command(id: Document_ID.Generic): Option[(Node, Command)] =
-          state.commands.get(id) orElse state.execs.get(id) match {
+          state.lookup_id(id) match {
             case None => None
             case Some(st) =>
               val command = st.command