src/Pure/General/base64.scala
author paulson <lp15@cam.ac.uk>
Mon, 25 Sep 2023 17:06:05 +0100
changeset 78698 1b9388e6eb75
parent 75620 44815dc2b8f9
child 80393 6138c5b803be
permissions -rw-r--r--
A few new theorems

/*  Title:      Pure/General/base64.scala
    Author:     Makarius

Support for Base64 data encoding.
*/

package isabelle


object Base64 {
  def encode(a: Array[Byte]): String = java.util.Base64.getEncoder.encodeToString(a)
  def decode(s: String): Array[Byte] = java.util.Base64.getDecoder.decode(s)


  /* Scala functions in ML */

  object Decode extends Scala.Fun_Bytes("Base64.decode") {
    val here = Scala_Project.here
    def apply(arg: Bytes): Bytes = Bytes.decode_base64(arg.text)
  }

  object Encode extends Scala.Fun_Bytes("Base64.encode") {
    val here = Scala_Project.here
    def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64)
  }
}