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;