src/Pure/General/url.scala
changeset 69394 f3240f3aa698
parent 67245 caa4c9001009
child 69901 20b32ade0024
equal deleted inserted replaced
69393:ed0824ef337e 69394:f3240f3aa698
    49   def read_gzip(url: URL): String = read(url, true)
    49   def read_gzip(url: URL): String = read(url, true)
    50 
    50 
    51   def read(name: String): String = read(Url(name), false)
    51   def read(name: String): String = read(Url(name), false)
    52   def read_gzip(name: String): String = read(Url(name), true)
    52   def read_gzip(name: String): String = read(Url(name), true)
    53 
    53 
       
    54   def read_bytes(url: URL): Bytes =
       
    55   {
       
    56     val connection = url.openConnection
       
    57     val length = connection.getContentLength
       
    58     using(connection.getInputStream)(Bytes.read_stream(_, hint = length))
       
    59   }
       
    60 
    54 
    61 
    55   /* file URIs */
    62   /* file URIs */
    56 
    63 
    57   def print_file(file: JFile): String = File.absolute(file).toPath.toUri.toString
    64   def print_file(file: JFile): String = File.absolute(file).toPath.toUri.toString
    58   def print_file_name(name: String): String = print_file(new JFile(name))
    65   def print_file_name(name: String): String = print_file(new JFile(name))