# HG changeset patch
# User wenzelm
# Date 1726050731 -7200
# Node ID b1ed84a5215b96fa430cfb3bea2910ce5e077665
# Parent  885343964b7f2247bd7e863f2ca0026d53105d40
clarified signature and modules;

diff -r 885343964b7f -r b1ed84a5215b src/Pure/PIDE/xml.ML
--- 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 =
diff -r 885343964b7f -r b1ed84a5215b src/Pure/PIDE/xml0.ML
--- a/src/Pure/PIDE/xml0.ML	Wed Sep 11 12:18:29 2024 +0200
+++ b/src/Pure/PIDE/xml0.ML	Wed Sep 11 12:32:11 2024 +0200
@@ -17,6 +17,8 @@
   val wrap_elem: ((string * attributes) * body) * body -> tree
   val unwrap_elem: tree -> (((string * attributes) * body) * body) option
   val unwrap_elem_body: tree -> body option
+  val traverse_text: (string -> 'a -> 'a) -> tree -> 'a -> 'a
+  val traverse_texts: (string -> 'a -> 'a) -> body -> 'a -> 'a
   val content_of: body -> string
 end
 
@@ -52,19 +54,19 @@
   | unwrap_elem_body _ = NONE;
 
 
-(* text content *)
+(* traverse text content *)
 
-fun add_contents [] res = res
-  | add_contents (t :: ts) res = add_contents ts (add_content t res)
-and add_content tree res =
+fun traverse_text f tree =
   (case unwrap_elem_body tree of
-    SOME ts => add_contents ts res
+    SOME ts => traverse_texts f ts
   | NONE =>
       (case tree of
-        Elem (_, ts) => add_contents ts res
-      | Text s => s :: res));
+        Elem (_, ts) => traverse_texts f ts
+      | Text s => f s))
+and traverse_texts _ [] res = res
+  | traverse_texts f (t :: ts) res = traverse_texts f ts (traverse_text f t res);
 
 fun content_of body =
-  String.concat (rev (add_contents body []));
+  String.concat (rev (traverse_texts (fn x => fn xs => x :: xs) body []));
 
 end;
diff -r 885343964b7f -r b1ed84a5215b src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Wed Sep 11 12:18:29 2024 +0200
+++ b/src/Tools/Code/code_printer.ML	Wed Sep 11 12:32:11 2024 +0200
@@ -138,10 +138,8 @@
 fun markup_stmt sym =
   Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]);
 
-val add_text = XML.traverse_text Bytes.add;
-
 fun filter_presentation [] xml =
-      Bytes.build (fold add_text xml)
+      Bytes.build (XML.traverse_texts Bytes.add xml)
   | filter_presentation presentation_syms xml =
       let
         val presentation_idents = map Code_Symbol.marker presentation_syms
@@ -151,7 +149,7 @@
         fun add_content_with_space tree (is_first, buf) =
           buf
           |> not is_first ? Bytes.add "\n\n"
-          |> add_text tree
+          |> XML.traverse_text Bytes.add tree
           |> pair false;
         fun filter (XML.Elem (name_attrs, xs)) =
               fold (if is_selected name_attrs then add_content_with_space else filter) xs