--- a/src/Pure/PIDE/xml.ML Wed Sep 11 12:18:29 2024 +0200
+++ b/src/Pure/PIDE/xml.ML Wed Sep 11 12:32:11 2024 +0200
@@ -37,7 +37,6 @@
val is_empty_body: body -> bool
val string: string -> body
val enclose: string -> string -> body -> body
- val traverse_text: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
val trim_blanks: body -> body
val filter_elements: {remove: string -> bool, expose: string -> bool} -> body -> body
val header: string
@@ -93,17 +92,6 @@
fun enclose bg en body = string bg @ body @ string en;
-(* traverse text *)
-
-fun traverse_text f tree =
- (case unwrap_elem_body tree of
- SOME ts => fold (traverse_text f) ts
- | NONE =>
- (case tree of
- Elem (_, ts) => fold (traverse_text f) ts
- | Text s => f s));
-
-
(* trim blanks *)
fun trim_blanks trees =