# HG changeset patch
# User wenzelm
# Date 1489703176 -3600
# Node ID fa62e095d8f1361d2b8e51ed2253dda202440f51
# Parent  b553d0edc440e53291b8ad12b16d14342306df61
clarified signature (again, see also 3ed43cfc8b14);

diff -r b553d0edc440 -r fa62e095d8f1 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Thu Mar 16 21:22:01 2017 +0100
+++ b/src/Pure/General/bytes.scala	Thu Mar 16 23:26:16 2017 +0100
@@ -110,9 +110,12 @@
 
   lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
 
+  def text: String =
+    UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
+
   override def toString: String =
   {
-    val str = UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
+    val str = text
     if (str.contains('\uFFFD')) "Bytes(" + length + ")" else str
   }