# 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 */