# HG changeset patch
# User wenzelm
# Date 1718475264 -7200
# Node ID 9db3959531061c747b7ede6d789ec4e7f9390b26
# Parent  a6c1526600b313ed9614d35dc0c92324e241e13f
clarified signature;

diff -r a6c1526600b3 -r 9db395953106 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Jun 15 17:16:14 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sat Jun 15 20:14:24 2024 +0200
@@ -363,7 +363,7 @@
 
   /* content */
 
-  def array: Array[Byte] = {
+  def make_array: Array[Byte] = {
     val buf = new ByteArrayOutputStream(small_size)
     for (a <- subarray_iterator) { buf.write(a.array, a.offset, a.length) }
     buf.toByteArray
@@ -372,7 +372,7 @@
   def text: String =
     if (is_empty) ""
     else if (byte_iterator.forall(_ >= 0)) {
-      new String(array, UTF8.charset)
+      new String(make_array, UTF8.charset)
     }
     else UTF8.decode_permissive_bytes(this)
 
@@ -383,7 +383,7 @@
     }
     catch { case ERROR(_) => None }
 
-  def encode_base64: String = Base64.encode(array)
+  def encode_base64: String = Base64.encode(make_array)
 
   def maybe_encode_base64: (Boolean, String) =
     wellformed_text match {
@@ -423,7 +423,7 @@
           else -1
         }
 
-        override def readAllBytes(): Array[Byte] = array
+        override def readAllBytes(): Array[Byte] = make_array
       }
     }
 
@@ -489,7 +489,7 @@
         Bytes(out.toByteArray)
       case options_zstd: Compress.Options_Zstd =>
         Zstd.init()
-        val inp = if (chunks.isEmpty && !is_sliced) chunk0 else array
+        val inp = if (chunks.isEmpty && !is_sliced) chunk0 else make_array
         Bytes(zstd.Zstd.compress(inp, options_zstd.level))
     }
   }
diff -r a6c1526600b3 -r 9db395953106 src/Pure/General/graphics_file.scala
--- a/src/Pure/General/graphics_file.scala	Sat Jun 15 17:16:14 2024 +0200
+++ b/src/Pure/General/graphics_file.scala	Sat Jun 15 20:14:24 2024 +0200
@@ -51,7 +51,7 @@
       val params = new DefaultFontMapper.BaseFontParameters(File.platform_path(entry.path))
       params.encoding = BaseFont.IDENTITY_H
       params.embedded = true
-      params.ttfAfm = entry.bytes.array
+      params.ttfAfm = entry.bytes.make_array
       mapper.putName(entry.name, params)
     }
     mapper
diff -r a6c1526600b3 -r 9db395953106 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Sat Jun 15 17:16:14 2024 +0200
+++ b/src/Pure/General/http.scala	Sat Jun 15 20:14:24 2024 +0200
@@ -50,7 +50,7 @@
     val encoding: String,
     val elapsed_time: Time
   ) {
-    def text: String = new String(bytes.array, encoding)
+    def text: String = new String(bytes.make_array, encoding)
     def json: JSON.T = JSON.parse(text)
   }
 
diff -r a6c1526600b3 -r 9db395953106 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Jun 15 17:16:14 2024 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sat Jun 15 20:14:24 2024 +0200
@@ -474,7 +474,7 @@
               else {
                 val bytes = using(zip_file.getInputStream(entry))(Bytes.read_stream(_))
                 Files.createDirectories(res.getParent)
-                Files.write(res, bytes.array)
+                Files.write(res, bytes.make_array)
               }
             }
             (entry, result)
diff -r a6c1526600b3 -r 9db395953106 src/Tools/VSCode/src/component_vscodium.scala
--- a/src/Tools/VSCode/src/component_vscodium.scala	Sat Jun 15 17:16:14 2024 +0200
+++ b/src/Tools/VSCode/src/component_vscodium.scala	Sat Jun 15 20:14:24 2024 +0200
@@ -229,7 +229,7 @@
   // function computeChecksum(filename)
   private def file_checksum(path: Path): String = {
     val digest = MessageDigest.getInstance("MD5")
-    digest.update(Bytes.read(path).array)
+    digest.update(Bytes.read(path).make_array)
     Bytes(Base64.getEncoder.encode(digest.digest()))
       .text.replaceAll("=", "")
   }