--- a/src/Pure/PIDE/xml.ML Tue Sep 10 19:57:45 2024 +0200
+++ b/src/Pure/PIDE/xml.ML Tue Sep 10 20:06:51 2024 +0200
@@ -37,7 +37,7 @@
val is_empty_body: body -> bool
val string: string -> body
val enclose: string -> string -> body -> body
- val add_content: tree -> Buffer.T -> Buffer.T
+ 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,15 +93,15 @@
fun enclose bg en body = string bg @ body @ string en;
-(* text content *)
+(* traverse text *)
-fun add_content tree =
+fun traverse_text f tree =
(case unwrap_elem_body tree of
- SOME ts => fold add_content ts
+ SOME ts => fold (traverse_text f) ts
| NONE =>
(case tree of
- Elem (_, ts) => fold add_content ts
- | Text s => Buffer.add s));
+ Elem (_, ts) => fold (traverse_text f) ts
+ | Text s => f s));
(* trim blanks *)
--- a/src/Tools/Code/code_printer.ML Tue Sep 10 19:57:45 2024 +0200
+++ b/src/Tools/Code/code_printer.ML Tue Sep 10 20:06:51 2024 +0200
@@ -138,8 +138,10 @@
fun markup_stmt sym =
Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]);
+val add_text = XML.traverse_text Buffer.add;
+
fun filter_presentation [] xml =
- Buffer.build (fold XML.add_content xml)
+ Buffer.build (fold add_text xml)
| filter_presentation presentation_syms xml =
let
val presentation_idents = map Code_Symbol.marker presentation_syms
@@ -149,7 +151,7 @@
fun add_content_with_space tree (is_first, buf) =
buf
|> not is_first ? Buffer.add "\n\n"
- |> XML.add_content tree
+ |> add_text tree
|> pair false;
fun filter (XML.Elem (name_attrs, xs)) =
fold (if is_selected name_attrs then add_content_with_space else filter) xs