tuned output;
authorwenzelm
Sun, 26 Mar 2023 19:31:05 +0200
changeset 77716 3f4163b83d4f
parent 77715 27dd3a3fcc54
child 77717 6a2daddc238c
tuned output;
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)