src/Pure/General/bytes.scala
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