| author | wenzelm | 
| Mon, 09 Sep 2024 22:59:51 +0200 | |
| changeset 80835 | abe1661ad692 | 
| parent 80834 | 28ed6ac50562 | 
| child 80836 | 7f989a84284a | 
--- a/src/Tools/Code/code_printer.ML Mon Sep 09 22:59:41 2024 +0200 +++ b/src/Tools/Code/code_printer.ML Mon Sep 09 22:59:51 2024 +0200 @@ -158,8 +158,8 @@ fun format presentation_names width = Pretty.output_buffer (Pretty.markup_output_ops (SOME width)) - #> Buffer.content - #> YXML.parse_body + #> Bytes.buffer + #> YXML.parse_body_bytes #> filter_presentation presentation_names #> Buffer.add "\n" #> Bytes.buffer;