# HG changeset patch
# User wenzelm
# Date 1726077972 -7200
# Node ID 96c895da5d8c066385cb6147c2b18db0ee444dac
# Parent  a392351d1ed432d5f2230cc466f26f7c4b13c495
tuned;

diff -r a392351d1ed4 -r 96c895da5d8c src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Wed Sep 11 20:05:09 2024 +0200
+++ b/src/Tools/Code/code_printer.ML	Wed Sep 11 20:06:12 2024 +0200
@@ -148,8 +148,8 @@
           |> not is_first ? Bytes.add "\n\n"
           |> 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
+        fun filter (XML.Elem (elem, body)) =
+              fold (if is_selected elem then add_content_with_space else filter) body
           | filter (XML.Text _) = I;
       in snd (fold filter xml (true, Bytes.empty)) end;