# HG changeset patch
# User wenzelm
# Date 1699737278 -3600
# Node ID b6116a86d2acc7d06f428ec10fb500af14aeed26
# Parent  4e1dc465dfccced2aca775b6fa162988354a78a8
clarified signature;

diff -r 4e1dc465dfcc -r b6116a86d2ac src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Nov 11 22:05:37 2023 +0100
+++ b/src/Pure/General/bytes.scala	Sat Nov 11 22:14:38 2023 +0100
@@ -72,13 +72,14 @@
 
   def read_url(name: String): Bytes = using(Url(name).openStream)(read_stream(_))
 
-  def read_file(file: JFile, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
+  def read_file(path: Path, offset: Long = 0L, limit: Long = Long.MaxValue): Bytes = {
+    val length = path.file.length
     val start = offset.max(0L)
-    val len = (file.length - start).max(0L).min(limit)
+    val len = (length - start).max(0L).min(limit)
     if (len > Int.MaxValue) error("Cannot read large file slice: " + Space.bytes(len).print)
     else if (len == 0L) empty
     else {
-      using(FileChannel.open(file.toPath, StandardOpenOption.READ)) { java_path =>
+      using(FileChannel.open(path.java_path, StandardOpenOption.READ)) { java_path =>
         java_path.position(start)
         val n = len.toInt
         val buf = ByteBuffer.allocate(n)
@@ -94,8 +95,8 @@
     }
   }
 
-  def read(file: JFile): Bytes = read_file(file)
-  def read(path: Path): Bytes = read_file(path.file)
+  def read(path: Path): Bytes = read_file(path)
+  def read(file: JFile): Bytes = read_file(File.path(file))
 
 
   /* write */
diff -r 4e1dc465dfcc -r b6116a86d2ac src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Sat Nov 11 22:05:37 2023 +0100
+++ b/src/Pure/ML/ml_heap.scala	Sat Nov 11 22:14:38 2023 +0100
@@ -22,7 +22,7 @@
       val l = sha1_prefix.length
       val m = l + SHA1.digest_length
       val n = heap.file.length
-      val bs = Bytes.read_file(heap.file, offset = n - m)
+      val bs = Bytes.read_file(heap, offset = n - m)
       if (bs.length == m) {
         val s = bs.text
         if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(l)))
@@ -166,7 +166,7 @@
             val offset = step * i
             val limit = if (j < slices) step * j else size
             val content =
-              Bytes.read_file(heap.file, offset = offset, limit = limit)
+              Bytes.read_file(heap, offset = offset, limit = limit)
                 .compress(cache = cache)
             private_data.transaction_lock(db, label = "ML_Heap.store2") {
               private_data.write_entry(db, session_name, i, content)