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