src/Pure/General/url.scala

--- a/src/Pure/General/url.scala	Tue Feb 28 16:26:05 2017 +0100
+++ b/src/Pure/General/url.scala	Tue Feb 28 17:48:28 2017 +0100
@@ -37,11 +37,8 @@
   /* read */
 
   private def read(url: URL, gzip: Boolean): String =
-  {
-    val stream = url.openStream
-    try { File.read_stream(if (gzip) new GZIPInputStream(stream) else stream) }
-    finally { stream.close }
-  }
+    using(url.openStream)(stream =>
+      File.read_stream(if (gzip) new GZIPInputStream(stream) else stream))
 
   def read(url: URL): String = read(url, false)
   def read_gzip(url: URL): String = read(url, true)