75620
|
1 |
/* Title: Pure/General/base64.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Support for Base64 data encoding.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
|
10 |
object Base64 {
|
|
11 |
def encode(a: Array[Byte]): String = java.util.Base64.getEncoder.encodeToString(a)
|
|
12 |
def decode(s: String): Array[Byte] = java.util.Base64.getDecoder.decode(s)
|
|
13 |
|
|
14 |
|
|
15 |
/* Scala functions in ML */
|
|
16 |
|
|
17 |
object Decode extends Scala.Fun_Bytes("Base64.decode") {
|
|
18 |
val here = Scala_Project.here
|
|
19 |
def apply(arg: Bytes): Bytes = Bytes.decode_base64(arg.text)
|
|
20 |
}
|
|
21 |
|
|
22 |
object Encode extends Scala.Fun_Bytes("Base64.encode") {
|
|
23 |
val here = Scala_Project.here
|
|
24 |
def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64)
|
|
25 |
}
|
|
26 |
}
|