src/Pure/General/http.scala
changeset 69305 5a71b5145201
parent 67865 ab0b8e388967
child 69355 cdc2de88d657
--- a/src/Pure/General/http.scala	Wed Nov 14 21:28:48 2018 +0100
+++ b/src/Pure/General/http.scala	Wed Nov 14 21:43:33 2018 +0100
@@ -45,13 +45,18 @@
     def request_uri: URI = http_exchange.getRequestURI
 
     def read_request(): Bytes =
-      using(http_exchange.getRequestBody)(Bytes.read_stream(_))
+    {
+      val stream = http_exchange.getRequestBody
+      try { Bytes.read_stream(stream) } finally { stream.close }
+    }
 
     def write_response(code: Int, response: Response)
     {
       http_exchange.getResponseHeaders().set("Content-Type", response.content_type)
       http_exchange.sendResponseHeaders(code, response.bytes.length.toLong)
-      using(http_exchange.getResponseBody)(response.bytes.write_stream(_))
+
+      val stream = http_exchange.getResponseBody
+      try { response.bytes.write_stream(stream) } finally { stream.close }
     }
   }