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