--- 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 = {