# HG changeset patch # User wenzelm # Date 1679851865 -7200 # Node ID 3f4163b83d4f612ae4518d0ff86d9074efd77f13 # Parent 27dd3a3fcc54933d1676ec6caaa3ee894599c6d6 tuned output; diff -r 27dd3a3fcc54 -r 3f4163b83d4f src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Sun Mar 26 15:47:40 2023 +0200 +++ b/src/Pure/General/bytes.scala Sun Mar 26 19:31:05 2023 +0200 @@ -174,7 +174,8 @@ case None => (true, encode_base64) } - override def toString: String = "Bytes(" + Space.bytes(length).print + ")" + override def toString: String = + if (is_empty) "Bytes.empty" else "Bytes(" + Space.bytes(length).print + ")" def proper: Option[Bytes] = if (is_empty) None else Some(this) def proper_text: Option[String] = if (is_empty) None else Some(text)