reactivated other_id reports (see also db929027e701, 8eda56033203);

--- a/NEWS	Wed Apr 20 11:33:45 2016 +0200
+++ b/NEWS	Wed Apr 20 11:44:25 2016 +0200
@@ -52,6 +52,10 @@
 
 * Highlighting of entity def/ref positions wrt. cursor.
 
+* Document markup works across multiple Isar commands, e.g. the results
+established at the end of a proof are properly identified in the theorem
+statement.
+
 
 *** Isar ***
 

--- 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) =>