# HG changeset patch
# User wenzelm
# Date 1470777575 -7200
# Node ID d7e0004d4321f03eddfb56cf9846bc2ea1bbca54
# Parent  ed266398da33b0f9e778680f6db55c13660048cf
more operations;

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)
 }