restrict report redirection to current node;

--- a/src/Pure/PIDE/command.scala	Sun Nov 29 16:21:27 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Nov 29 16:45:29 2020 +0100
@@ -261,7 +261,8 @@
 
     def accumulate(
         self_id: Document_ID.Generic => Boolean,
-        other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
+        other_id: (Document.Node.Name, Document_ID.Generic) =>
+          Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
         message: XML.Elem,
         xml_cache: XML.Cache): State =
       message match {
@@ -293,7 +294,8 @@
                       val target =
                         if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
                           Some((chunk_name, command.chunks(chunk_name)))
-                        else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
+                        else if (chunk_name == Symbol.Text_Chunk.Default)
+                          other_id(command.node_name, id)
                         else None
 
                       (target, atts) match {

--- a/src/Pure/PIDE/document.scala	Sun Nov 29 16:21:27 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Nov 29 16:45:29 2020 +0100
@@ -752,9 +752,14 @@
       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)
+    private def other_id(node_name: Node.Name, id: Document_ID.Generic)
       : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] =
-      lookup_id(id).map(st => ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)))
+    {
+      for {
+        st <- lookup_id(id)
+        if st.command.node_name == node_name
+      } yield (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) =>