src/Pure/General/base64.scala
author wenzelm
Sat, 25 Jun 2022 13:19:15 +0200
changeset 75620 44815dc2b8f9
child 80393 6138c5b803be
permissions -rw-r--r--
clarified modules;
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
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     4
Support for Base64 data encoding.
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
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    10
object Base64 {
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    11
  def encode(a: Array[Byte]): String = java.util.Base64.getEncoder.encodeToString(a)
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    12
  def decode(s: String): Array[Byte] = java.util.Base64.getDecoder.decode(s)
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    13
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    14
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    15
  /* Scala functions in ML */
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    16
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    17
  object Decode extends Scala.Fun_Bytes("Base64.decode") {
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    18
    val here = Scala_Project.here
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    19
    def apply(arg: Bytes): Bytes = Bytes.decode_base64(arg.text)
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    20
  }
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    21
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    22
  object Encode extends Scala.Fun_Bytes("Base64.encode") {
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    23
    val here = Scala_Project.here
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    24
    def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64)
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    25
  }
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    26
}