src/Pure/General/bytes.scala
changeset 71350 f2d848a596d1
parent 71349 69a22ccd1817
child 73122 1b0f81e556a2
equal deleted inserted replaced
71349:69a22ccd1817 71350:f2d848a596d1
    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(_, limit = file.length.toInt))
    69   {
       
    70     val length = file.length
       
    71     val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt
       
    72     using(new FileInputStream(file))(read_stream(_, limit = limit))
       
    73   }
    70 
    74 
    71   def read(path: Path): Bytes = read(path.file)
    75   def read(path: Path): Bytes = read(path.file)
    72 
    76 
    73   def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
    77   def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
    74 
    78