author | wenzelm |
Sun, 14 Jul 2024 17:56:54 +0200 | |
changeset 80567 | b2c14b489e60 |
parent 80566 | 446b887e23c7 |
child 80568 | fbb655bf62d4 |
--- a/src/Pure/General/bytes.ML Sun Jul 14 17:49:30 2024 +0200 +++ b/src/Pure/General/bytes.ML Sun Jul 14 17:56:54 2024 +0200 @@ -216,6 +216,8 @@ val _ = ML_system_pp (fn _ => fn _ => fn bytes => - PolyML.PrettyString ("Bytes {size = " ^ string_of_int (size bytes) ^ "}")) + PolyML.PrettyString + (if is_empty bytes then "Bytes.empty" + else "Bytes {size = " ^ string_of_int (size bytes) ^ "}")) end;