src/Pure/General/http.scala
changeset 73416 08aa4c1ed579
parent 73413 56c0a793cd8b
child 73417 1dcc2b228b8b
--- 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 */