src/Pure/General/base64.scala
changeset 75620 44815dc2b8f9
child 80393 6138c5b803be
equal deleted inserted replaced
75619:9639c3867b86 75620:44815dc2b8f9
       
     1 /*  Title:      Pure/General/base64.scala
       
     2     Author:     Makarius
       
     3 
       
     4 Support for Base64 data encoding.
       
     5 */
       
     6 
       
     7 package isabelle
       
     8 
       
     9 
       
    10 object Base64 {
       
    11   def encode(a: Array[Byte]): String = java.util.Base64.getEncoder.encodeToString(a)
       
    12   def decode(s: String): Array[Byte] = java.util.Base64.getDecoder.decode(s)
       
    13 
       
    14 
       
    15   /* Scala functions in ML */
       
    16 
       
    17   object Decode extends Scala.Fun_Bytes("Base64.decode") {
       
    18     val here = Scala_Project.here
       
    19     def apply(arg: Bytes): Bytes = Bytes.decode_base64(arg.text)
       
    20   }
       
    21 
       
    22   object Encode extends Scala.Fun_Bytes("Base64.encode") {
       
    23     val here = Scala_Project.here
       
    24     def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64)
       
    25   }
       
    26 }