# HG changeset patch
# User wenzelm
# Date 1725915591 -7200
# Node ID abe1661ad6920a7937acd11784d5dca3e045ac1d
# Parent  28ed6ac50562b5df3baad6c2cbcb07b9ec5ec85a
more scalable;

diff -r 28ed6ac50562 -r abe1661ad692 src/Tools/Code/code_printer.ML
--- 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;