# HG changeset patch # User wenzelm # Date 1543846554 -3600 # Node ID f3240f3aa698bc9de6db3b16c07e27ba66e8fbcf # Parent ed0824ef337ecfcd4286b86bb57230e526c94cbc more operations; diff -r ed0824ef337e -r f3240f3aa698 src/Pure/General/url.scala --- a/src/Pure/General/url.scala Mon Dec 03 14:59:42 2018 +0100 +++ b/src/Pure/General/url.scala Mon Dec 03 15:15:54 2018 +0100 @@ -51,6 +51,13 @@ def read(name: String): String = read(Url(name), false) def read_gzip(name: String): String = read(Url(name), true) + def read_bytes(url: URL): Bytes = + { + val connection = url.openConnection + val length = connection.getContentLength + using(connection.getInputStream)(Bytes.read_stream(_, hint = length)) + } + /* file URIs */