src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Wed Apr 20 11:33:45 2016 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Apr 20 11:44:25 2016 +0200
@@ -564,11 +564,9 @@
       (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)] = None
-    /* FIXME
+      : 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)))
-    */
 
     private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
       (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>