# HG changeset patch
# User wenzelm
# Date 1525642234 -7200
# Node ID 0b66aca9c9657097ed1440fcc957617b1a95dc07
# Parent  b98c5877b0f323a849fc1bcc13b77ea08a260094
more operations;

diff -r b98c5877b0f3 -r 0b66aca9c965 src/Pure/General/bytes.scala
--- 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