--- 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 {