more scalable;
authorwenzelm
Mon, 09 Sep 2024 22:59:51 +0200
changeset 80835 abe1661ad692
parent 80834 28ed6ac50562
child 80836 7f989a84284a
more scalable;
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;