# HG changeset patch
# User wenzelm
# Date 1718556117 -7200
# Node ID 6138c5b803be61c3d868c4fee7c4b9acc4ab9a6b
# Parent  c22a56495b4c4c0df3dd3a1ead00050afea0136d
Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);

diff -r c22a56495b4c -r 6138c5b803be src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Sun Jun 16 18:18:55 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Sun Jun 16 18:41:57 2024 +0200
@@ -1174,7 +1174,7 @@
       val head =
         List(
           HTML.title("Isabelle Build Manager"),
-          Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64),
+          Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64.text),
           HTML.style_file("https://hawkz.github.io/gdcss/gd.css"),
           HTML.style("html { background-color: white; }"))
     }
diff -r c22a56495b4c -r 6138c5b803be src/Pure/General/base64.scala
--- a/src/Pure/General/base64.scala	Sun Jun 16 18:18:55 2024 +0200
+++ b/src/Pure/General/base64.scala	Sun Jun 16 18:41:57 2024 +0200
@@ -1,26 +1,34 @@
 /*  Title:      Pure/General/base64.scala
     Author:     Makarius
 
-Support for Base64 data encoding.
+Support for Base64 data representation.
 */
 
 package isabelle
 
 
+import java.io.{InputStream, OutputStream}
+
+
 object Base64 {
+  /* main operations */
+
   def encode(a: Array[Byte]): String = java.util.Base64.getEncoder.encodeToString(a)
   def decode(s: String): Array[Byte] = java.util.Base64.getDecoder.decode(s)
 
+  def encode_stream(s: OutputStream): OutputStream = java.util.Base64.getEncoder.wrap(s)
+  def decode_stream(s: InputStream): InputStream = java.util.Base64.getDecoder.wrap(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)
+    def apply(bytes: Bytes): Bytes = bytes.decode_base64
   }
 
   object Encode extends Scala.Fun_Bytes("Base64.encode") {
     val here = Scala_Project.here
-    def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64)
+    def apply(bytes: Bytes): Bytes = bytes.encode_base64
   }
 }
diff -r c22a56495b4c -r 6138c5b803be src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sun Jun 16 18:18:55 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sun Jun 16 18:41:57 2024 +0200
@@ -55,8 +55,6 @@
 
   val newline: Bytes = apply("\n")
 
-  def decode_base64(s: String): Bytes = Bytes.reuse_array(Base64.decode(s))
-
 
   /* read */
 
@@ -441,12 +439,22 @@
     }
     catch { case ERROR(_) => None }
 
-  def encode_base64: String = Base64.encode(make_array)
+
+  /* Base64 data representation */
+
+  def encode_base64: Bytes = {
+    val out = new Bytes.Builder.Stream(hint = (size * 1.5).round)
+    using(Base64.encode_stream(out))(write_stream(_))
+    out.builder.done()
+  }
+
+  def decode_base64: Bytes =
+    using(Base64.decode_stream(stream()))(Bytes.read_stream(_, hint = (size / 1.2).round))
 
   def maybe_encode_base64: (Boolean, String) =
     wellformed_text match {
       case Some(s) => (false, s)
-      case None => (true, encode_base64)
+      case None => (true, encode_base64.text)
     }