clarified signature: more explicit HTTP operations;

--- a/src/Pure/General/http.scala	Fri Mar 12 19:43:49 2021 +0100
+++ b/src/Pure/General/http.scala	Fri Mar 12 19:46:37 2021 +0100
@@ -7,14 +7,42 @@
 package isabelle
 
 
-import java.net.{InetAddress, InetSocketAddress, URI}
+import java.net.{InetSocketAddress, URI, URL}
 import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
 
-import scala.collection.immutable.SortedMap
-
 
 object HTTP
 {
+  /** content **/
+
+  val default_mime_type: String = "application/octet-stream"
+
+  sealed case class Content(bytes: Bytes, mime_type: String = default_mime_type)
+  {
+    def text: String = bytes.text
+  }
+
+
+
+  /** client **/
+
+  object Client
+  {
+    def get(url: URL): Content =
+    {
+      val connection = url.openConnection
+      using(connection.getInputStream)(stream =>
+      {
+        val length = connection.getContentLength
+        val mime_type = Option(connection.getContentType).getOrElse(default_mime_type)
+        val bytes = Bytes.read_stream(stream, hint = length)
+        Content(bytes, mime_type = mime_type)
+      })
+    }
+  }
+
+
+
   /** server **/
 
   /* response */

--- a/src/Pure/General/url.scala	Fri Mar 12 19:43:49 2021 +0100
+++ b/src/Pure/General/url.scala	Fri Mar 12 19:46:37 2021 +0100
@@ -80,13 +80,6 @@
   def read(name: String): String = read(Url(name), false)
   def read_gzip(name: String): String = read(Url(name), true)
 
-  def read_bytes(url: URL): Bytes =
-  {
-    val connection = url.openConnection
-    val length = connection.getContentLength
-    using(connection.getInputStream)(Bytes.read_stream(_, hint = length))
-  }
-
 
   /* file URIs */
 

--- a/src/Pure/System/isabelle_system.scala	Fri Mar 12 19:43:49 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Fri Mar 12 19:46:37 2021 +0100
@@ -551,10 +551,10 @@
   {
     val url = Url(url_name)
     progress.echo("Getting " + quote(url_name))
-    val bytes =
-      try { Url.read_bytes(url) }
+    val content =
+      try { HTTP.Client.get(url) }
       catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
-    Bytes.write(file, bytes)
+    Bytes.write(file, content.bytes)
   }
 
   object Download extends Scala.Fun("download")