clarified treatment of non-text bytes;
authorwenzelm
Sat, 15 Oct 2016 15:23:06 +0200
changeset 64224 3ed43cfc8b14
parent 64223 9d5b9f41df77
child 64225 d78d46c755f8
clarified treatment of non-text bytes;
src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Oct 15 15:14:46 2016 +0200
+++ b/src/Pure/General/bytes.scala	Sat Oct 15 15:23:06 2016 +0200
@@ -96,7 +96,10 @@
   lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
 
   override def toString: String =
-    UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
+  {
+    val str = UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
+    if (str.contains('\uFFFD')) "Bytes(" + length + ")" else str
+  }
 
   def isEmpty: Boolean = length == 0