src/Pure/General/base64.scala
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--
clarified: more uniform;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
75620
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/base64.scala
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     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
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     6
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     8
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     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
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    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
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    16
  def encode(a: Array[Byte]): String = java.util.Base64.getEncoder.encodeToString(a)
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    17
  def decode(s: String): Array[Byte] = java.util.Base64.getDecoder.decode(s)
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    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
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    22
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    23
  /* Scala functions in ML */
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    24
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    25
  object Decode extends Scala.Fun_Bytes("Base64.decode") {
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    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
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    28
  }
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    29
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    30
  object Encode extends Scala.Fun_Bytes("Base64.encode") {
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    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
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    33
  }
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    34
}