changeset 68106 | a514e29db980 |
parent 68094 | 0b66aca9c965 |
child 68108 | 2277fe496d78 |
--- a/src/Pure/General/bytes.scala Mon May 07 18:25:26 2018 +0200 +++ b/src/Pure/General/bytes.scala Mon May 07 19:40:55 2018 +0200 @@ -160,6 +160,12 @@ Base64.getEncoder.encodeToString(b) } + def maybe_base64: (Boolean, String) = + { + val s = text + if (this == Bytes(s)) (false, s) else (true, base64) + } + override def toString: String = { val str = text