equal
deleted
inserted
replaced
|
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 } |