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