# HG changeset patch
# User wenzelm
# Date 1725643049 -7200
# Node ID 84e8867925367117a4ca1154724377a3aed1f627
# Parent  da2557168da77e5157e8fabe0dde853870df4618
more accurate output, following 3f02bc5a5a03;

diff -r da2557168da7 -r 84e886792536 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 }
 }