# HG changeset patch
# User wenzelm
# Date 1679833478 -7200
# Node ID 25fd62cba3477a686a97cb49c09d9d5de19da8d4
# Parent  b8b01343e3dfb79f6dc8b5e081f240dc8507aea4
clarified signature: more general operation Bytes.read_slice;

diff -r b8b01343e3df -r 25fd62cba347 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sun Mar 26 12:53:53 2023 +0200
+++ b/src/Pure/General/bytes.scala	Sun Mar 26 14:24:38 2023 +0200
@@ -9,6 +9,9 @@
 
 import java.io.{ByteArrayInputStream, ByteArrayOutputStream, FileInputStream, FileOutputStream, InputStream, OutputStream, File as JFile}
 import java.net.URL
+import java.nio.ByteBuffer
+import java.nio.channels.FileChannel
+import java.nio.file.StandardOpenOption
 import org.tukaani.xz
 import com.github.luben.zstd
 
@@ -75,6 +78,28 @@
 
   def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
 
+  def read_slice(path: Path, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
+    val start = offset.max(0L)
+    val len = (path.file.length - start).max(0L).min(limit)
+    if (len > Integer.MAX_VALUE) error("Cannot read large file slice: " + Space.bytes(len).print)
+    else if (len == 0L) empty
+    else {
+      using(FileChannel.open(path.java_path, StandardOpenOption.READ)) { file =>
+        file.position(start)
+        val n = len.toInt
+        val buf = ByteBuffer.allocate(n)
+        var i = 0
+        var m = 0
+        while ({
+          m = file.read(buf)
+          if (m != -1) i += m
+          m != -1 && n > i
+        }) ()
+        new Bytes(buf.array, 0, i)
+      }
+    }
+  }
+
 
   /* write */
 
diff -r b8b01343e3df -r 25fd62cba347 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Sun Mar 26 12:53:53 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Sun Mar 26 14:24:38 2023 +0200
@@ -19,30 +19,16 @@
 
   def read_digest(heap: Path): Option[SHA1.Digest] = {
     if (heap.is_file) {
-      using(FileChannel.open(heap.java_path, StandardOpenOption.READ)) { file =>
-        val len = file.size
-        val n = sha1_prefix.length + SHA1.digest_length
-        if (len >= n) {
-          file.position(len - n)
-
-          val buf = ByteBuffer.allocate(n)
-          var i = 0
-          var m = 0
-          while ({
-            m = file.read(buf)
-            if (m != -1) i += m
-            m != -1 && n > i
-          }) ()
-
-          if (i == n) {
-            val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
-            val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset)
-            if (prefix == sha1_prefix) Some(SHA1.fake_digest(s)) else None
-          }
-          else None
-        }
+      val l = sha1_prefix.length
+      val m = l + SHA1.digest_length
+      val n = heap.file.length
+      val bs = Bytes.read_slice(heap, offset = n - m)
+      if (bs.length == m) {
+        val s = bs.text
+        if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(l)))
         else None
       }
+      else None
     }
     else None
   }