clarified signature (again, see also 3ed43cfc8b14);
authorwenzelm
Thu, 16 Mar 2017 23:26:16 +0100
changeset 65279 fa62e095d8f1
parent 65278 b553d0edc440
child 65280 ef37f5236794
clarified signature (again, see also 3ed43cfc8b14);
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
   }