src/Pure/PIDE/protocol_message.scala

--- a/src/Pure/PIDE/protocol_message.scala	Fri Sep 06 19:08:44 2024 +0200
+++ b/src/Pure/PIDE/protocol_message.scala	Fri Sep 06 19:17:29 2024 +0200
@@ -60,6 +60,11 @@
   /* clean output */
 
   def clean_output(msg: String): String =
-    try { XML.content(clean_reports(YXML.parse_body(YXML.Source(msg)))) }
+    try {
+      XML.content(
+        XML.filter_elements(YXML.parse_body(YXML.Source(msg)),
+          remove = Markup.Elements(Markup.REPORT),
+          expose = no_report_elements))
+    }
     catch { case ERROR(_) => msg }
 }