# HG changeset patch
# User wenzelm
# Date 1476537786 -7200
# Node ID 3ed43cfc8b14f7a87c827a4818b7e2297e1b4d42
# Parent  9d5b9f41df77949ee193247e7d3c548703b55fcf
clarified treatment of non-text bytes;

diff -r 9d5b9f41df77 -r 3ed43cfc8b14 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