src/Pure/General/bytes.scala
changeset 71151 69a22ccd1817
parent 69454 ef051edd4d10
child 71152 f2d848a596d1
equal deleted inserted replaced
71150:9e7d40d67258 71151:69a22ccd1817
    64 
    64 
    65       new Bytes(out.toByteArray, 0, out.size)
    65       new Bytes(out.toByteArray, 0, out.size)
    66     }
    66     }
    67 
    67 
    68   def read(file: JFile): Bytes =
    68   def read(file: JFile): Bytes =
    69     using(new FileInputStream(file))(read_stream(_, file.length.toInt))
    69     using(new FileInputStream(file))(read_stream(_, limit = file.length.toInt))
    70 
    70 
    71   def read(path: Path): Bytes = read(path.file)
    71   def read(path: Path): Bytes = read(path.file)
    72 
    72 
    73   def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
    73   def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
    74 
    74