more operations;

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