src/Pure/General/bytes.scala
changeset 68106 a514e29db980
parent 68094 0b66aca9c965
child 68108 2277fe496d78
equal deleted inserted replaced
68105:577072a0ceed 68106:a514e29db980
   158       if (offset == 0 && length == bytes.length) bytes
   158       if (offset == 0 && length == bytes.length) bytes
   159       else Bytes(bytes, offset, length).bytes
   159       else Bytes(bytes, offset, length).bytes
   160     Base64.getEncoder.encodeToString(b)
   160     Base64.getEncoder.encodeToString(b)
   161   }
   161   }
   162 
   162 
       
   163   def maybe_base64: (Boolean, String) =
       
   164   {
       
   165     val s = text
       
   166     if (this == Bytes(s)) (false, s) else (true, base64)
       
   167   }
       
   168 
   163   override def toString: String =
   169   override def toString: String =
   164   {
   170   {
   165     val str = text
   171     val str = text
   166     if (str.contains('\uFFFD')) "Bytes(" + length + ")" else str
   172     if (str.contains('\uFFFD')) "Bytes(" + length + ")" else str
   167   }
   173   }