src/Pure/PIDE/protocol_message.scala
changeset 80455 99e276c44121
parent 75393 87ebf5a50283
child 80816 774e5a0c4c9e
--- a/src/Pure/PIDE/protocol_message.scala	Sat Jun 29 12:42:47 2024 +0200
+++ b/src/Pure/PIDE/protocol_message.scala	Sat Jun 29 12:50:43 2024 +0200
@@ -64,7 +64,7 @@
         List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
       case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
         List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
-      case XML.Wrapped_Elem(_, _, ts) => reports(props, ts)
+      case XML.Wrapped_Elem_Body(ts) => reports(props, ts)
       case XML.Elem(_, ts) => reports(props, ts)
       case XML.Text(_) => Nil
     }