author | Fabian Huch <huch@in.tum.de> |
Thu, 18 Jul 2024 13:08:11 +0200 | |
changeset 80574 | 90493e889dff |
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 |
} |