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