clarified output: avoid costly operations on huge blobs;
authorwenzelm
Fri May 11 20:05:37 2018 +0200 (12 months ago)
changeset 68150f0f34cbed539
parent 68149 9a4a6adb95b5
child 68151 3c321783bae3
clarified output: avoid costly operations on huge blobs;
src/Pure/General/bytes.scala
     1.1 --- a/src/Pure/General/bytes.scala	Fri May 11 19:59:05 2018 +0200
     1.2 +++ b/src/Pure/General/bytes.scala	Fri May 11 20:05:37 2018 +0200
     1.3 @@ -156,11 +156,7 @@
     1.4      if (this == Bytes(s)) (false, s) else (true, base64)
     1.5    }
     1.6  
     1.7 -  override def toString: String =
     1.8 -  {
     1.9 -    val str = text
    1.10 -    if (str.contains('\uFFFD')) "Bytes(" + length + ")" else str
    1.11 -  }
    1.12 +  override def toString: String = "Bytes(" + length + ")"
    1.13  
    1.14    def isEmpty: Boolean = length == 0
    1.15