diff -r ed266398da33 -r d7e0004d4321 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Tue Aug 09 23:18:42 2016 +0200
+++ b/src/Pure/General/url.scala	Tue Aug 09 23:19:35 2016 +0200
@@ -33,13 +33,16 @@
 
   /* read */
 
-  private def gen_read(name: String, gzip: Boolean): String =
+  private def read(url: URL, gzip: Boolean): String =
   {
-    val stream = Url(name).openStream
+    val stream = url.openStream
     try { File.read_stream(if (gzip) new GZIPInputStream(stream) else stream) }
     finally { stream.close }
   }
 
-  def read(name: String): String = gen_read(name, false)
-  def read_gzip(name: String): String = gen_read(name, true)
+  def read(url: URL): String = read(url, false)
+  def read_gzip(url: URL): String = read(url, true)
+
+  def read(name: String): String = read(Url(name), false)
+  def read_gzip(name: String): String = read(Url(name), true)
 }