# HG changeset patch
# User wenzelm
# Date 1679853095 -7200
# Node ID 6ad3a412ed976931d6f018530b7e0ff7ac3c9cc7
# Parent  6a2daddc238c4561d3660ef788af32dd2297fb34
clarified signature;

diff -r 6a2daddc238c -r 6ad3a412ed97 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sun Mar 26 19:36:00 2023 +0200
+++ b/src/Pure/General/bytes.scala	Sun Mar 26 19:51:35 2023 +0200
@@ -71,28 +71,20 @@
 
   def read_url(name: String): Bytes = using(Url(name).openStream)(read_stream(_))
 
-  def read(file: JFile): Bytes = {
-    val length = file.length
-    val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt
-    using(new FileInputStream(file))(read_stream(_, limit = limit))
-  }
-
-  def read(path: Path): Bytes = read(path.file)
-
-  def read_slice(path: Path, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
+  def read_file(file: JFile, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
     val start = offset.max(0L)
-    val len = (path.file.length - start).max(0L).min(limit)
+    val len = (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)
+      using(FileChannel.open(file.toPath, StandardOpenOption.READ)) { java_path =>
+        java_path.position(start)
         val n = len.toInt
         val buf = ByteBuffer.allocate(n)
         var i = 0
         var m = 0
         while ({
-          m = file.read(buf)
+          m = java_path.read(buf)
           if (m != -1) i += m
           m != -1 && n > i
         }) ()
@@ -101,6 +93,9 @@
     }
   }
 
+  def read(file: JFile): Bytes = read_file(file)
+  def read(path: Path): Bytes = read_file(path.file)
+
 
   /* write */
 
diff -r 6a2daddc238c -r 6ad3a412ed97 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Sun Mar 26 19:36:00 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Sun Mar 26 19:51:35 2023 +0200
@@ -22,7 +22,7 @@
       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)
+      val bs = Bytes.read_file(heap.file, offset = n - m)
       if (bs.length == m) {
         val s = bs.text
         if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(l)))