--- a/src/Pure/General/bytes.scala Sun May 06 23:03:43 2018 +0200
+++ b/src/Pure/General/bytes.scala Sun May 06 23:30:34 2018 +0200
@@ -10,6 +10,7 @@
import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream,
OutputStream, InputStream, FileInputStream, FileOutputStream}
import java.net.URL
+import java.util.Base64
import org.tukaani.xz.{XZInputStream, XZOutputStream}
@@ -151,6 +152,14 @@
def text: String =
UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
+ def base64: String =
+ {
+ val b =
+ if (offset == 0 && length == bytes.length) bytes
+ else Bytes(bytes, offset, length).bytes
+ Base64.getEncoder.encodeToString(b)
+ }
+
override def toString: String =
{
val str = text