# 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("=", "") }