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 */