| author | wenzelm | 
| Tue, 10 Dec 2024 21:06:04 +0100 | |
| changeset 81572 | 693a95492008 | 
| 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: 
75620diff
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: 
75620diff
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: 
75620diff
changeset | 11 | |
| 
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
 wenzelm parents: 
75620diff
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: 
75620diff
changeset | 14 | /* main operations */ | 
| 
6138c5b803be
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);
 wenzelm parents: 
75620diff
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: 
75620diff
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: 
75620diff
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: 
75620diff
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: 
75620diff
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: 
75620diff
changeset | 32 | def apply(bytes: Bytes): Bytes = bytes.encode_base64 | 
| 75620 | 33 | } | 
| 34 | } |