src/Pure/General/http.scala
author wenzelm
Wed, 31 Mar 2021 12:02:52 +0200
changeset 73774 c42144d9dde6
parent 73692 3696bb4085ed
child 73779 2cd23d587db9
permissions -rw-r--r--
more uniform HTTP resources;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
     1
/*  Title:      Pure/General/http.scala
63823
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     3
73690
69d449f0ca04 tuned comments;
wenzelm
parents: 73682
diff changeset
     4
HTTP client and server support.
63823
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     5
*/
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     6
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     7
package isabelle
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     8
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
     9
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    10
import java.io.{File => JFile}
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    11
import java.net.{InetSocketAddress, URI, URL, URLConnection, HttpURLConnection}
63823
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    12
import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    13
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    14
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
    15
object HTTP
63823
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    16
{
73668
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
    17
  /** content **/
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
    18
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    19
  val mime_type_bytes: String = "application/octet-stream"
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    20
  val mime_type_text: String = "text/plain; charset=utf-8"
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    21
  val mime_type_html: String = "text/html; charset=utf-8"
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    22
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    23
  val default_mime_type: String = mime_type_bytes
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    24
  val default_encoding: String = UTF8.charset_name
73668
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
    25
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    26
  sealed case class Content(
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    27
    bytes: Bytes,
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    28
    file_name: String = "",
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    29
    mime_type: String = default_mime_type,
73681
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73677
diff changeset
    30
    encoding: String = default_encoding,
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73677
diff changeset
    31
    elapsed_time: Time = Time.zero)
73668
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
    32
  {
73692
3696bb4085ed tuned signature (again);
wenzelm
parents: 73691
diff changeset
    33
    def text: String = new String(bytes.array, encoding)
73668
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
    34
  }
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
    35
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    36
  def read_content(file: JFile): Content =
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    37
  {
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    38
    val bytes = Bytes.read(file)
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    39
    val file_name = file.getName
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    40
    val mime_type =
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    41
      Option(URLConnection.guessContentTypeFromName(file_name)).getOrElse(default_mime_type)
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    42
    Content(bytes, file_name = file_name, mime_type = mime_type)
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    43
  }
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    44
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    45
  def read_content(path: Path): Content = read_content(path.file)
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    46
73668
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
    47
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
    48
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
    49
  /** client **/
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
    50
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    51
  val NEWLINE: String = "\r\n"
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    52
73668
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
    53
  object Client
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
    54
  {
73691
cb127ce2c092 tuned --- following hints by IntelliJ;
wenzelm
parents: 73690
diff changeset
    55
    val default_timeout: Time = Time.seconds(180)
73674
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
    56
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
    57
    def open_connection(url: URL,
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
    58
      timeout: Time = default_timeout,
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
    59
      user_agent: String = ""): HttpURLConnection =
73673
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
    60
    {
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
    61
      url.openConnection match {
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
    62
        case connection: HttpURLConnection =>
73674
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
    63
          if (0 < timeout.ms && timeout.ms <= Integer.MAX_VALUE) {
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
    64
            val ms = timeout.ms.toInt
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
    65
            connection.setConnectTimeout(ms)
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
    66
            connection.setReadTimeout(ms)
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
    67
          }
73673
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
    68
          proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s))
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
    69
          connection
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
    70
        case _ => error("Bad URL (not HTTP): " + quote(url.toString))
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
    71
      }
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
    72
    }
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    73
73673
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
    74
    def get_content(connection: HttpURLConnection): Content =
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    75
    {
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    76
      val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r
73681
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73677
diff changeset
    77
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73677
diff changeset
    78
      val start = Time.now()
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    79
      using(connection.getInputStream)(stream =>
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    80
      {
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    81
        val bytes = Bytes.read_stream(stream, hint = connection.getContentLength)
73681
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73677
diff changeset
    82
        val stop = Time.now()
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73677
diff changeset
    83
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    84
        val file_name = Url.file_name(connection.getURL)
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    85
        val mime_type = Option(connection.getContentType).getOrElse(default_mime_type)
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    86
        val encoding =
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    87
          (connection.getContentEncoding, mime_type) match {
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    88
            case (enc, _) if enc != null => enc
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    89
            case (_, Charset(enc)) => enc
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    90
            case _ => default_encoding
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    91
          }
73681
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73677
diff changeset
    92
        Content(bytes, file_name = file_name, mime_type = mime_type,
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73677
diff changeset
    93
          encoding = encoding, elapsed_time = stop - start)
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    94
      })
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    95
    }
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    96
73674
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
    97
    def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content =
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
    98
      get_content(open_connection(url, timeout = timeout, user_agent = user_agent))
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
    99
73674
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
   100
    def post(url: URL, parameters: List[(String, Any)],
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
   101
      timeout: Time = default_timeout,
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
   102
      user_agent: String = ""): Content =
73668
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
   103
    {
73674
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73673
diff changeset
   104
      val connection = open_connection(url, timeout = timeout, user_agent = user_agent)
73673
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   105
      connection.setRequestMethod("POST")
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   106
      connection.setDoOutput(true)
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
   107
73673
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   108
      val boundary = UUID.random_string()
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   109
      connection.setRequestProperty(
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   110
        "Content-Type", "multipart/form-data; boundary=" + quote(boundary))
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
   111
73673
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   112
      using(connection.getOutputStream)(out =>
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   113
      {
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   114
        def output(s: String): Unit = out.write(UTF8.bytes(s))
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   115
        def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE))
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   116
        def output_boundary(end: Boolean = false): Unit =
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   117
          output("--" + boundary + (if (end) "--" else "") + NEWLINE)
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   118
        def output_name(name: String): Unit =
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   119
          output("Content-Disposition: form-data; name=" + quote(name))
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   120
        def output_value(value: Any): Unit =
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   121
        {
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   122
          output_newline(2)
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   123
          output(value.toString)
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   124
        }
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   125
        def output_content(content: Content): Unit =
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   126
        {
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   127
          proper_string(content.file_name).foreach(s => output("; filename=" + quote(s)))
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   128
          output_newline()
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   129
          proper_string(content.mime_type).foreach(s => output("Content-Type: " + s))
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   130
          output_newline(2)
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   131
          content.bytes.write_stream(out)
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   132
        }
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
   133
73673
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   134
        output_newline(2)
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
   135
73673
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   136
        for { (name, value) <- parameters } {
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   137
          output_boundary()
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   138
          output_name(name)
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   139
          value match {
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   140
            case content: Content => output_content(content)
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   141
            case file: JFile => output_content(read_content(file))
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   142
            case path: Path => output_content(read_content(path))
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   143
            case _ => output_value(value)
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   144
          }
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   145
          output_newline()
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   146
        }
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   147
        output_boundary(end = true)
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   148
        out.flush()
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   149
      })
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
   150
73673
a114ecd280ca clarified signature;
wenzelm
parents: 73669
diff changeset
   151
      get_content(connection)
73668
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
   152
    }
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
   153
  }
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
   154
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
   155
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73665
diff changeset
   156
65081
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   157
  /** server **/
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   158
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   159
  /* response */
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   160
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   161
  object Response
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   162
  {
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   163
    def apply(
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   164
        bytes: Bytes = Bytes.empty,
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
   165
        content_type: String = mime_type_bytes): Response =
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   166
      new Response(bytes, content_type)
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   167
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   168
    val empty: Response = apply()
73669
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
   169
    def text(s: String): Response = apply(Bytes(s), mime_type_text)
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73668
diff changeset
   170
    def html(s: String): Response = apply(Bytes(s), mime_type_html)
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   171
  }
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   172
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   173
  class Response private[HTTP](val bytes: Bytes, val content_type: String)
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   174
  {
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   175
    override def toString: String = bytes.toString
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   176
  }
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   177
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   178
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   179
  /* exchange */
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   180
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   181
  class Exchange private[HTTP](val http_exchange: HttpExchange)
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   182
  {
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   183
    def request_method: String = http_exchange.getRequestMethod
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   184
    def request_uri: URI = http_exchange.getRequestURI
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   185
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   186
    def read_request(): Bytes =
69403
ed0824ef337e static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents: 69384
diff changeset
   187
      using(http_exchange.getRequestBody)(Bytes.read_stream(_))
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   188
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 69473
diff changeset
   189
    def write_response(code: Int, response: Response): Unit =
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   190
    {
73691
cb127ce2c092 tuned --- following hints by IntelliJ;
wenzelm
parents: 73690
diff changeset
   191
      http_exchange.getResponseHeaders.set("Content-Type", response.content_type)
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   192
      http_exchange.sendResponseHeaders(code, response.bytes.length.toLong)
73691
cb127ce2c092 tuned --- following hints by IntelliJ;
wenzelm
parents: 73690
diff changeset
   193
      using(http_exchange.getResponseBody)(response.bytes.write_stream)
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   194
    }
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   195
  }
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   196
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   197
73665
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   198
  /* handler for request method */
66207
8d5cb4ea2b7c support for HTTP/POST method;
wenzelm
parents: 66001
diff changeset
   199
8d5cb4ea2b7c support for HTTP/POST method;
wenzelm
parents: 66001
diff changeset
   200
  sealed case class Arg(method: String, uri: URI, request: Bytes)
8d5cb4ea2b7c support for HTTP/POST method;
wenzelm
parents: 66001
diff changeset
   201
  {
8d5cb4ea2b7c support for HTTP/POST method;
wenzelm
parents: 66001
diff changeset
   202
    def decode_properties: Properties.T =
66923
wenzelm
parents: 66479
diff changeset
   203
      space_explode('&', request.text).map(s =>
wenzelm
parents: 66479
diff changeset
   204
        space_explode('=', s) match {
67245
caa4c9001009 tuned signature;
wenzelm
parents: 66923
diff changeset
   205
          case List(a, b) => Url.decode(a) -> Url.decode(b)
66207
8d5cb4ea2b7c support for HTTP/POST method;
wenzelm
parents: 66001
diff changeset
   206
          case _ => error("Malformed key-value pair in HTTP/POST: " + quote(s))
8d5cb4ea2b7c support for HTTP/POST method;
wenzelm
parents: 66001
diff changeset
   207
        })
8d5cb4ea2b7c support for HTTP/POST method;
wenzelm
parents: 66001
diff changeset
   208
  }
8d5cb4ea2b7c support for HTTP/POST method;
wenzelm
parents: 66001
diff changeset
   209
73665
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   210
  object Handler
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   211
  {
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   212
    def apply(root: String, body: Exchange => Unit): Handler =
73691
cb127ce2c092 tuned --- following hints by IntelliJ;
wenzelm
parents: 73690
diff changeset
   213
      new Handler(root, (x: HttpExchange) => body(new Exchange(x)))
73665
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   214
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   215
    def method(name: String, root: String, body: Arg => Option[Response]): Handler =
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   216
      apply(root, http =>
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   217
        {
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   218
          val request = http.read_request()
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   219
          if (http.request_method == name) {
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   220
            val arg = Arg(name, http.request_uri, request)
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   221
            Exn.capture(body(arg)) match {
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   222
              case Exn.Res(Some(response)) =>
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   223
                http.write_response(200, response)
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   224
              case Exn.Res(None) =>
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   225
                http.write_response(404, Response.empty)
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   226
              case Exn.Exn(ERROR(msg)) =>
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   227
                http.write_response(500, Response.text(Output.error_message_text(msg)))
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   228
              case Exn.Exn(exn) => throw exn
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   229
            }
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   230
          }
73665
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   231
          else http.write_response(400, Response.empty)
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   232
        })
65076
8a96ab58f016 clarified signature;
wenzelm
parents: 63823
diff changeset
   233
73665
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   234
    def get(root: String, body: Arg => Option[Response]): Handler = method("GET", root, body)
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   235
    def post(root: String, body: Arg => Option[Response]): Handler = method("POST", root, body)
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   236
  }
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   237
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   238
  class Handler private(val root: String, val handler: HttpHandler)
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   239
  {
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   240
    override def toString: String = root
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   241
  }
66207
8d5cb4ea2b7c support for HTTP/POST method;
wenzelm
parents: 66001
diff changeset
   242
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   243
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   244
  /* server */
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   245
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   246
  class Server private[HTTP](val http_server: HttpServer)
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   247
  {
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 69473
diff changeset
   248
    def += (handler: Handler): Unit = http_server.createContext(handler.root, handler.handler)
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 69473
diff changeset
   249
    def -= (handler: Handler): Unit = http_server.removeContext(handler.root)
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   250
73691
cb127ce2c092 tuned --- following hints by IntelliJ;
wenzelm
parents: 73690
diff changeset
   251
    def start(): Unit = http_server.start()
73614
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   252
    def stop(): Unit = http_server.stop(0)
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   253
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   254
    def address: InetSocketAddress = http_server.getAddress
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   255
    def url: String = "http://" + address.getHostName + ":" + address.getPort
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   256
    override def toString: String = url
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   257
  }
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   258
65081
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   259
  def server(handlers: List[Handler] = isabelle_resources): Server =
63823
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
   260
  {
69473
6439c9024dcc clarified signature;
wenzelm
parents: 69403
diff changeset
   261
    val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0)
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   262
    http_server.setExecutor(null)
65076
8a96ab58f016 clarified signature;
wenzelm
parents: 63823
diff changeset
   263
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   264
    val server = new Server(http_server)
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   265
    for (handler <- handlers) server += handler
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   266
    server
63823
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
   267
  }
65079
8a5c2b86c5f6 handler for Isabelle fonts;
wenzelm
parents: 65078
diff changeset
   268
8a5c2b86c5f6 handler for Isabelle fonts;
wenzelm
parents: 65078
diff changeset
   269
65081
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   270
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   271
  /** Isabelle resources **/
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   272
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   273
  lazy val isabelle_resources: List[Handler] =
73774
c42144d9dde6 more uniform HTTP resources;
wenzelm
parents: 73692
diff changeset
   274
    List(welcome(), fonts())
65081
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   275
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   276
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   277
  /* welcome */
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   278
73774
c42144d9dde6 more uniform HTTP resources;
wenzelm
parents: 73692
diff changeset
   279
  def welcome(root: String = "/"): Handler =
c42144d9dde6 more uniform HTTP resources;
wenzelm
parents: 73692
diff changeset
   280
    Handler.get(root, arg =>
c42144d9dde6 more uniform HTTP resources;
wenzelm
parents: 73692
diff changeset
   281
      if (arg.uri.toString == root) {
67865
ab0b8e388967 more uniform id;
wenzelm
parents: 67245
diff changeset
   282
        val id = Isabelle_System.isabelle_id()
65084
23202c455a3e tuned message;
wenzelm
parents: 65083
diff changeset
   283
        Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version))
65081
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   284
      }
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   285
      else None)
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   286
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   287
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   288
  /* fonts */
65079
8a5c2b86c5f6 handler for Isabelle fonts;
wenzelm
parents: 65078
diff changeset
   289
69384
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69376
diff changeset
   290
  private lazy val html_fonts: List[Isabelle_Fonts.Entry] =
ab66951166f3 clarified "hidden" terminology;
wenzelm
parents: 69376
diff changeset
   291
    Isabelle_Fonts.fonts(hidden = true)
65079
8a5c2b86c5f6 handler for Isabelle fonts;
wenzelm
parents: 65078
diff changeset
   292
8a5c2b86c5f6 handler for Isabelle fonts;
wenzelm
parents: 65078
diff changeset
   293
  def fonts(root: String = "/fonts"): Handler =
73665
56c0a793cd8b clarified signature;
wenzelm
parents: 73614
diff changeset
   294
    Handler.get(root, arg =>
65079
8a5c2b86c5f6 handler for Isabelle fonts;
wenzelm
parents: 65078
diff changeset
   295
      {
66479
5c0a3f63057d proper argument type (amending 8d5cb4ea2b7c);
wenzelm
parents: 66207
diff changeset
   296
        val uri_name = arg.uri.toString
69374
91dbade9a5fa proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents: 69373
diff changeset
   297
        if (uri_name == root) {
69376
b6dacf6eabe3 clarified signature;
wenzelm
parents: 69374
diff changeset
   298
          Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name))))
69374
91dbade9a5fa proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents: 69373
diff changeset
   299
        }
91dbade9a5fa proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents: 69373
diff changeset
   300
        else {
91dbade9a5fa proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents: 69373
diff changeset
   301
          html_fonts.collectFirst(
69376
b6dacf6eabe3 clarified signature;
wenzelm
parents: 69374
diff changeset
   302
            { case entry if uri_name == root + "/" + entry.path.file_name => Response(entry.bytes) })
69374
91dbade9a5fa proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents: 69373
diff changeset
   303
        }
65079
8a5c2b86c5f6 handler for Isabelle fonts;
wenzelm
parents: 65078
diff changeset
   304
      })
63823
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
   305
}