# HG changeset patch
# User wenzelm
# Date 1725630411 -7200
# Node ID 774e5a0c4c9eedbd96af29bb7462d29c8a006655
# Parent  cd10c7c9f25c4d959523b8143a5c41a9cb5b4e28
misc tuning and clarification;

diff -r cd10c7c9f25c -r 774e5a0c4c9e src/Pure/PIDE/protocol_message.scala
--- a/src/Pure/PIDE/protocol_message.scala	Fri Sep 06 14:47:42 2024 +0200
+++ b/src/Pure/PIDE/protocol_message.scala	Fri Sep 06 15:46:51 2024 +0200
@@ -36,27 +36,14 @@
 
   /* inlined reports */
 
-  private val report_elements =
-    Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
+  private val report_elements = Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
+  private val no_report_elements = Markup.Elements(Markup.NO_REPORT)
 
   def clean_reports(body: XML.Body): XML.Body =
-    body filter {
-      case XML.Wrapped_Elem(Markup(name, _), _, _) => !report_elements(name)
-      case XML.Elem(Markup(name, _), _) => !report_elements(name)
-      case _ => true
-    } map {
-      case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_reports(ts))
-      case XML.Elem(markup, ts) => XML.Elem(markup, clean_reports(ts))
-      case t => t
-    }
+    XML.clean_elements(report_elements, body, full = true)
 
   def expose_no_reports(body: XML.Body): XML.Body =
-    body flatMap {
-      case XML.Wrapped_Elem(markup, body, ts) => List(XML.Wrapped_Elem(markup, body, expose_no_reports(ts)))
-      case XML.Elem(Markup(Markup.NO_REPORT, _), ts) => ts
-      case XML.Elem(markup, ts) => List(XML.Elem(markup, expose_no_reports(ts)))
-      case t => List(t)
-    }
+    XML.clean_elements(no_report_elements, body)
 
   def reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
     body flatMap {
diff -r cd10c7c9f25c -r 774e5a0c4c9e src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Fri Sep 06 14:47:42 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Fri Sep 06 15:46:51 2024 +0200
@@ -139,6 +139,25 @@
   }
 
 
+  /* clean markup elements */
+
+  def clean_elements(elements: Markup.Elements, xml: XML.Body, full: Boolean = false): XML.Body = {
+    def clean(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
+        case XML.Elem(markup, body) =>
+          if (!elements(markup.name)) Some(XML.Elem(markup, clean(body)))
+          else if (!full) clean(body)
+          else Nil
+        case t => List(t)
+      }
+    clean(xml)
+  }
+
+
   /* traverse text */
 
   def traverse_text[A](body: Body, a: A, op: (A, String) => A): A = {