diff -r 23d2adc5489e -r b50f8cc8c08e src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Mon Apr 12 22:45:38 2021 +0200 +++ b/src/Pure/General/bytes.scala Mon Apr 12 22:57:39 2021 +0200 @@ -41,12 +41,29 @@ val newline: Bytes = apply("\n") + + /* base64 */ + def base64(s: String): Bytes = { val a = Base64.getDecoder.decode(s) new Bytes(a, 0, a.length) } + object Decode_Base64 extends Scala.Fun("decode_base64") + { + val here = Scala_Project.here + def invoke(args: List[Bytes]): List[Bytes] = + List(base64(Library.the_single(args).text)) + } + + object Encode_Base64 extends Scala.Fun("encode_base64") + { + val here = Scala_Project.here + def invoke(args: List[Bytes]): List[Bytes] = + List(Bytes(Library.the_single(args).base64)) + } + /* read */