src/Pure/General/bytes.scala

--- a/src/Pure/General/bytes.scala	Sat Jun 25 10:27:42 2022 +0200
+++ b/src/Pure/General/bytes.scala	Sat Jun 25 13:19:15 2022 +0200
@@ -10,7 +10,6 @@
 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}
 
@@ -43,33 +42,10 @@
   /* base64 */
 
   def decode_base64(s: String): Bytes = {
-    val a = Base64.getDecoder.decode(s)
+    val a = Base64.decode(s)
     new Bytes(a, 0, a.length)
   }
 
-  object Decode_Base64 extends Scala.Fun_Bytes("decode_base64") {
-    val here = Scala_Project.here
-    def apply(arg: Bytes): Bytes = decode_base64(arg.text)
-  }
-
-  object Encode_Base64 extends Scala.Fun_Bytes("encode_base64") {
-    val here = Scala_Project.here
-    def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64)
-  }
-
-
-  /* XZ compression */
-
-  object Compress extends Scala.Fun_Bytes("compress") {
-    val here = Scala_Project.here
-    def apply(arg: Bytes): Bytes = arg.compress()
-  }
-
-  object Uncompress extends Scala.Fun_Bytes("uncompress") {
-    val here = Scala_Project.here
-    def apply(arg: Bytes): Bytes = arg.uncompress()
-  }
-
 
   /* read */
 
@@ -160,7 +136,7 @@
     val b =
       if (offset == 0 && length == bytes.length) bytes
       else Bytes(bytes, offset, length).bytes
-    Base64.getEncoder.encodeToString(b)
+    Base64.encode(b)
   }
 
   def maybe_encode_base64: (Boolean, String) = {