tuned;
authorwenzelm
Thu, 13 Jun 2024 15:08:24 +0200
changeset 80364 d5c48fe601b6
parent 80363 306f273c91ec
child 80365 29b761e290c5
tuned;
src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Wed Jun 12 22:09:16 2024 +0200
+++ b/src/Pure/General/bytes.scala	Thu Jun 13 15:08:24 2024 +0200
@@ -76,14 +76,14 @@
     if (len > Int.MaxValue) error("Cannot read large file slice: " + Space.bytes(len).print)
     else if (len == 0L) empty
     else {
-      using(FileChannel.open(path.java_path, StandardOpenOption.READ)) { java_path =>
-        java_path.position(start)
+      using(FileChannel.open(path.java_path, StandardOpenOption.READ)) { channel =>
+        channel.position(start)
         val n = len.toInt
         val buf = ByteBuffer.allocate(n)
         var i = 0
         var m = 0
         while ({
-          m = java_path.read(buf)
+          m = channel.read(buf)
           if (m != -1) i += m
           m != -1 && n > i
         }) ()