# HG changeset patch
# User wenzelm
# Date 1655819791 -7200
# Node ID 06f8b072f28ef42ef545fe62ef7541f9583701c7
# Parent  5945c6f5126a65274a897ec4d70ec847f1f6af31
clarified ML pretty printing;

diff -r 5945c6f5126a -r 06f8b072f28e src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Tue Jun 21 15:48:59 2022 +0200
+++ b/src/Pure/General/bytes.ML	Tue Jun 21 15:56:31 2022 +0200
@@ -97,4 +97,8 @@
 val read = File.open_input read_stream;
 val write = File.open_output write_stream;
 
+val _ =
+  ML_system_pp (fn _ => fn _ => fn bytes =>
+    PolyML.PrettyString ("Bytes {length = " ^ string_of_int (length bytes) ^ "}"))
+
 end;