src/Pure/General/base64.ML
author wenzelm
Sun, 09 Jul 2023 14:33:45 +0200
changeset 78273 95a3bb4d7e38
parent 76183 8089593a364a
permissions -rw-r--r--
clarified "vacuum" operation for various database versions (PostgreSQL <= 10 is strictly speaking obsolete, but still used on some test machines);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
76183
8089593a364a proper file headers;
wenzelm
parents: 75621
diff changeset
     1
(*  Title:      Pure/General/base64.ML
75620
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 (via Isabelle/Scala).
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     5
*)
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     6
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     7
signature BASE64 =
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     8
sig
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
     9
  val decode: Bytes.T -> Bytes.T
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    10
  val encode: Bytes.T -> Bytes.T
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    11
end;
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    12
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    13
structure Base64: BASE64 =
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    14
struct
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    15
75621
aeb412065742 prefer antiquotations;
wenzelm
parents: 75620
diff changeset
    16
val decode = \<^scala>\<open>Base64.decode\<close>;
aeb412065742 prefer antiquotations;
wenzelm
parents: 75620
diff changeset
    17
val encode = \<^scala>\<open>Base64.encode\<close>;
75620
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    18
44815dc2b8f9 clarified modules;
wenzelm
parents:
diff changeset
    19
end;