diff -r 9ed32b8a03a9 -r 93c2058896a4 src/Tools/Code/code_printer.ML
--- 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