diff -r 0cc96d337e8f -r cb9d5af781b4 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Nov 25 15:24:55 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Nov 25 16:14:16 2020 +0100
@@ -345,13 +345,14 @@
               })
           }
 
-        case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
+        case XML.Elem(Markup(Markup.REPORT, atts0), msgs) =>
           (this /: msgs)((state, msg) =>
             {
               def bad(): Unit = Output.warning("Ignored report message: " + msg)
 
               msg match {
-                case XML.Elem(Markup(name, atts), args) =>
+                case XML.Elem(Markup(name, atts1), args) =>
+                  val atts = atts1 ::: atts0
                   command.reported_position(atts) match {
                     case Some((id, chunk_name)) =>
                       val target =