# HG changeset patch
# User wenzelm
# Date 1726143876 -7200
# Node ID 9a7de3f320d8570cd7a3fcf0a7fa39c988cdc10a
# Parent  87395be1a299744eefb68041b933f2edb7f16778
clarified signature;

diff -r 87395be1a299 -r 9a7de3f320d8 src/Pure/PIDE/protocol_message.scala
--- a/src/Pure/PIDE/protocol_message.scala	Thu Sep 12 13:13:59 2024 +0200
+++ b/src/Pure/PIDE/protocol_message.scala	Thu Sep 12 14:24:36 2024 +0200
@@ -36,11 +36,12 @@
 
   /* inlined reports */
 
-  private val report_elements = Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
-  private val no_report_elements = Markup.Elements(Markup.NO_REPORT)
+  val report_elements: Markup.Elements = Markup.Elements(Markup.REPORT)
+  val no_report_elements: Markup.Elements = Markup.Elements(Markup.NO_REPORT)
+  val any_report_elements: Markup.Elements = Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
 
   def clean_reports(body: XML.Body): XML.Body =
-    XML.filter_elements(body, remove = report_elements)
+    XML.filter_elements(body, remove = any_report_elements)
 
   def expose_no_reports(body: XML.Body): XML.Body =
     XML.filter_elements(body, expose = no_report_elements)
@@ -63,7 +64,7 @@
     try {
       XML.content(
         XML.filter_elements(YXML.parse_body(YXML.Source(msg)),
-          remove = Markup.Elements(Markup.REPORT),
+          remove = report_elements,
           expose = no_report_elements))
     }
     catch { case ERROR(_) => msg }