# HG changeset patch
# User wenzelm
# Date 1470767721 -7200
# Node ID d83a1eeff9d2b4293747e35a22c8adc88c8d5e5a
# Parent  7205aaf670ad3bf8d65c188bd521914215a47be5
more operations;

diff -r 7205aaf670ad -r d83a1eeff9d2 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Tue Aug 09 19:45:01 2016 +0200
+++ b/src/Pure/General/url.scala	Tue Aug 09 20:35:21 2016 +0200
@@ -8,6 +8,7 @@
 
 
 import java.net.{URL, MalformedURLException}
+import java.util.zip.GZIPInputStream
 
 
 object Url
@@ -29,11 +30,16 @@
     try { Url(name).openStream.close; true }
     catch { case ERROR(_) => false }
 
-  def read(name: String): String =
+
+  /* read */
+
+  private def gen_read(name: String, gzip: Boolean): String =
   {
     val stream = Url(name).openStream
-    try { File.read_stream(stream) }
+    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)
 }
-