--- 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 **)