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