clarified signature;

--- a/src/Pure/PIDE/protocol_message.scala	Fri Sep 06 15:59:48 2024 +0200
+++ b/src/Pure/PIDE/protocol_message.scala	Fri Sep 06 19:08:44 2024 +0200
@@ -40,10 +40,10 @@
   private val no_report_elements = Markup.Elements(Markup.NO_REPORT)
 
   def clean_reports(body: XML.Body): XML.Body =
-    XML.clean_elements(report_elements, body, full = true)
+    XML.filter_elements(body, remove = report_elements)
 
   def expose_no_reports(body: XML.Body): XML.Body =
-    XML.clean_elements(no_report_elements, body)
+    XML.filter_elements(body, expose = no_report_elements)
 
   def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
     body flatMap {

--- a/src/Pure/PIDE/xml.scala	Fri Sep 06 15:59:48 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Fri Sep 06 19:08:44 2024 +0200
@@ -139,22 +139,25 @@
   }
 
 
-  /* clean markup elements */
+  /* filter markup elements */
 
-  def clean_elements(elements: Markup.Elements, xml: XML.Body, full: Boolean = false): XML.Body = {
-    def clean(ts: XML.Body): XML.Body =
+  def filter_elements(xml: XML.Body,
+    remove: Markup.Elements = Markup.Elements.empty,
+    expose: Markup.Elements = Markup.Elements.empty
+  ): XML.Body = {
+    def filter(ts: XML.Body): XML.Body =
       ts flatMap {
         case XML.Wrapped_Elem(markup, body1, body2) =>
-          if (!elements(markup.name)) Some(XML.Wrapped_Elem(markup, body1, clean(body2)))
-          else if (!full) clean(body2)
-          else Nil
+          if (remove(markup.name)) Nil
+          else if (expose(markup.name)) filter(body2)
+          else List(XML.Wrapped_Elem(markup, body1, filter(body2)))
         case XML.Elem(markup, body) =>
-          if (!elements(markup.name)) Some(XML.Elem(markup, clean(body)))
-          else if (!full) clean(body)
-          else Nil
+          if (remove(markup.name)) Nil
+          else if (expose(markup.name)) filter(body)
+          else List(XML.Elem(markup, filter(body)))
         case t => List(t)
       }
-    clean(xml)
+    filter(xml)
   }