src/Pure/PIDE/xml.ML
changeset 80820 db114ec720cb
parent 80809 4a64fc4d1cde
child 80838 aaf9e8a392cc
--- a/src/Pure/PIDE/xml.ML	Fri Sep 06 19:17:29 2024 +0200
+++ b/src/Pure/PIDE/xml.ML	Fri Sep 06 20:31:20 2024 +0200
@@ -39,6 +39,7 @@
   val enclose: string -> string -> body -> body
   val add_content: tree -> Buffer.T -> Buffer.T
   val trim_blanks: body -> body
+  val filter_elements: {remove: string -> bool, expose: string -> bool} -> body -> body
   val header: string
   val text: string -> string
   val element: string -> attributes -> string list -> string
@@ -111,6 +112,26 @@
       | Text s => s |> raw_explode |> trim Symbol.is_blank |> implode |> string);
 
 
+(* filter markup elements *)
+
+fun filter_elements {remove, expose} =
+  let
+    fun filter ts =
+      ts |> maps (fn t =>
+        (case XML.unwrap_elem t of
+          SOME ((markup, body1), body2) =>
+            if remove (#1 markup) then []
+            else if expose (#1 markup) then filter body2
+            else [XML.wrap_elem ((markup, body1), filter body2)]
+        | NONE =>
+            (case t of
+              XML.Elem (markup, body) =>
+                if remove (#1 markup) then []
+                else if expose (#1 markup) then filter body
+                else [XML.Elem (markup, filter body)]
+            | _ => [t])));
+  in filter end;
+
 
 (** string representation **)