| author | wenzelm |
| Fri, 25 Oct 2024 16:03:58 +0200 | |
| changeset 81261 | 0c9075bdff38 |
| parent 80393 | 6138c5b803be |
| permissions | -rw-r--r-- |
| 75620 | 1 |
/* Title: Pure/General/base64.scala |
2 |
Author: Makarius |
|
3 |
||
|
80393
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
wenzelm
parents:
75620
diff
changeset
|
4 |
Support for Base64 data representation. |
| 75620 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
|
80393
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
wenzelm
parents:
75620
diff
changeset
|
10 |
import java.io.{InputStream, OutputStream}
|
|
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
wenzelm
parents:
75620
diff
changeset
|
11 |
|
|
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
wenzelm
parents:
75620
diff
changeset
|
12 |
|
| 75620 | 13 |
object Base64 {
|
|
80393
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
wenzelm
parents:
75620
diff
changeset
|
14 |
/* main operations */ |
|
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
wenzelm
parents:
75620
diff
changeset
|
15 |
|
| 75620 | 16 |
def encode(a: Array[Byte]): String = java.util.Base64.getEncoder.encodeToString(a) |
17 |
def decode(s: String): Array[Byte] = java.util.Base64.getDecoder.decode(s) |
|
18 |
||
|
80393
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
wenzelm
parents:
75620
diff
changeset
|
19 |
def encode_stream(s: OutputStream): OutputStream = java.util.Base64.getEncoder.wrap(s) |
|
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
wenzelm
parents:
75620
diff
changeset
|
20 |
def decode_stream(s: InputStream): InputStream = java.util.Base64.getDecoder.wrap(s) |
|
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
wenzelm
parents:
75620
diff
changeset
|
21 |
|
| 75620 | 22 |
|
23 |
/* Scala functions in ML */ |
|
24 |
||
25 |
object Decode extends Scala.Fun_Bytes("Base64.decode") {
|
|
26 |
val here = Scala_Project.here |
|
|
80393
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
wenzelm
parents:
75620
diff
changeset
|
27 |
def apply(bytes: Bytes): Bytes = bytes.decode_base64 |
| 75620 | 28 |
} |
29 |
||
30 |
object Encode extends Scala.Fun_Bytes("Base64.encode") {
|
|
31 |
val here = Scala_Project.here |
|
|
80393
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
wenzelm
parents:
75620
diff
changeset
|
32 |
def apply(bytes: Bytes): Bytes = bytes.encode_base64 |
| 75620 | 33 |
} |
34 |
} |