support for base64 via Isabelle/Scala/ML;

--- a/src/Pure/General/bytes.scala	Mon Apr 12 22:45:38 2021 +0200
+++ b/src/Pure/General/bytes.scala	Mon Apr 12 22:57:39 2021 +0200
@@ -41,12 +41,29 @@
 
   val newline: Bytes = apply("\n")
 
+
+  /* base64 */
+
   def base64(s: String): Bytes =
   {
     val a = Base64.getDecoder.decode(s)
     new Bytes(a, 0, a.length)
   }
 
+  object Decode_Base64 extends Scala.Fun("decode_base64")
+  {
+    val here = Scala_Project.here
+    def invoke(args: List[Bytes]): List[Bytes] =
+      List(base64(Library.the_single(args).text))
+  }
+
+  object Encode_Base64 extends Scala.Fun("encode_base64")
+  {
+    val here = Scala_Project.here
+    def invoke(args: List[Bytes]): List[Bytes] =
+      List(Bytes(Library.the_single(args).base64))
+  }
+
 
   /* read */
 

--- a/src/Pure/System/isabelle_system.ML	Mon Apr 12 22:45:38 2021 +0200
+++ b/src/Pure/System/isabelle_system.ML	Mon Apr 12 22:57:39 2021 +0200
@@ -121,6 +121,12 @@
 fun download_file url path = File.write path (download url);
 
 
+(* base64 *)
+
+val decode_base64 = Scala.function1 "decode_base64";
+val encode_base64 = Scala.function1 "encode_base64";
+
+
 (* Isabelle distribution identification *)
 
 fun isabelle_id () = Scala.function1 "isabelle_id" "";

--- a/src/Pure/System/scala.scala	Mon Apr 12 22:45:38 2021 +0200
+++ b/src/Pure/System/scala.scala	Mon Apr 12 22:57:39 2021 +0200
@@ -267,6 +267,8 @@
   Scala.Echo,
   Scala.Sleep,
   Scala.Toplevel,
+  Bytes.Decode_Base64,
+  Bytes.Encode_Base64,
   Doc.Doc_Names,
   Bash.Process,
   Bibtex.Check_Database,