src/Pure/General/http.scala
author wenzelm
Sun, 02 Jul 2023 19:05:59 +0200
changeset 78243 0e221a8128e4
parent 76356 92e9fa289056
child 78768 280a228dc2f1
permissions -rw-r--r--
tuned: prefer Scala over Java;
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
73438
69d449f0ca04 tuned comments;
wenzelm
parents: 73430
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
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    10
import java.io.{File => JFile}
75104
08bb0d32b2e3 more robust mime_type;
wenzelm
parents: 74945
diff changeset
    11
import java.nio.file.Files
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
    12
import java.net.{InetSocketAddress, URI, URL, HttpURLConnection}
63823
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    13
import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    14
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
    15
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
    16
object HTTP {
73416
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
    17
  /** content **/
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
    18
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
    19
  object Content {
75106
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    20
    val mime_type_bytes: String = "application/octet-stream"
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    21
    val mime_type_text: String = "text/plain; charset=utf-8"
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    22
    val mime_type_html: String = "text/html; charset=utf-8"
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    23
75106
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    24
    val default_mime_type: String = mime_type_bytes
76356
92e9fa289056 tuned signature;
wenzelm
parents: 76270
diff changeset
    25
    val default_encoding: String = UTF8.charset.name
75106
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    26
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    27
    def apply(
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    28
        bytes: Bytes,
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    29
        file_name: String = "",
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    30
        mime_type: String = default_mime_type,
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    31
        encoding: String = default_encoding,
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    32
        elapsed_time: Time = Time.zero): Content =
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    33
      new Content(bytes, file_name, mime_type, encoding, elapsed_time)
73416
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
    34
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
    35
    def read(file: JFile): Content = {
75106
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    36
      val bytes = Bytes.read(file)
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    37
      val file_name = file.getName
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    38
      val mime_type = Option(Files.probeContentType(file.toPath)).getOrElse(default_mime_type)
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    39
      apply(bytes, file_name = file_name, mime_type = mime_type)
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    40
    }
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    41
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    42
    def read(path: Path): Content = read(path.file)
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    43
  }
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    44
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    45
  class Content private(
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    46
    val bytes: Bytes,
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    47
    val file_name: String,
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    48
    val mime_type: String,
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    49
    val encoding: String,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
    50
    val elapsed_time: Time
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
    51
  ) {
73440
3696bb4085ed tuned signature (again);
wenzelm
parents: 73439
diff changeset
    52
    def text: String = new String(bytes.array, encoding)
74945
4dc90b43ba94 support for Flarum server;
wenzelm
parents: 74094
diff changeset
    53
    def json: JSON.T = JSON.parse(text)
73416
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
    54
  }
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
    55
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
    56
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
    57
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
    58
  /** client **/
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
    59
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    60
  val NEWLINE: String = "\r\n"
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    61
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
    62
  object Client {
73439
cb127ce2c092 tuned --- following hints by IntelliJ;
wenzelm
parents: 73438
diff changeset
    63
    val default_timeout: Time = Time.seconds(180)
73422
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73421
diff changeset
    64
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
    65
    def open_connection(
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
    66
      url: URL,
73422
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73421
diff changeset
    67
      timeout: Time = default_timeout,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
    68
      user_agent: String = ""
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
    69
    ): HttpURLConnection = {
73421
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
    70
      url.openConnection match {
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
    71
        case connection: HttpURLConnection =>
78243
0e221a8128e4 tuned: prefer Scala over Java;
wenzelm
parents: 76356
diff changeset
    72
          if (0 < timeout.ms && timeout.ms <= Int.MaxValue) {
73422
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73421
diff changeset
    73
            val ms = timeout.ms.toInt
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73421
diff changeset
    74
            connection.setConnectTimeout(ms)
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73421
diff changeset
    75
            connection.setReadTimeout(ms)
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73421
diff changeset
    76
          }
73421
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
    77
          proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s))
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
    78
          connection
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
    79
        case _ => error("Bad URL (not HTTP): " + quote(url.toString))
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
    80
      }
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
    81
    }
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    82
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
    83
    def get_content(connection: HttpURLConnection): Content = {
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    84
      val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r
73429
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73425
diff changeset
    85
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73425
diff changeset
    86
      val start = Time.now()
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    87
      using(connection.getInputStream) { stream =>
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    88
        val bytes = Bytes.read_stream(stream, hint = connection.getContentLength)
73429
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73425
diff changeset
    89
        val stop = Time.now()
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73425
diff changeset
    90
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    91
        val file_name = Url.file_name(connection.getURL)
75106
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    92
        val mime_type = Option(connection.getContentType).getOrElse(Content.default_mime_type)
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    93
        val encoding =
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    94
          (connection.getContentEncoding, mime_type) match {
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    95
            case (enc, _) if enc != null => enc
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    96
            case (_, Charset(enc)) => enc
75106
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
    97
            case _ => Content.default_encoding
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
    98
          }
73429
8970081c6500 elapsed time to download content (and for the server to provide content);
wenzelm
parents: 73425
diff changeset
    99
        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: 73425
diff changeset
   100
          encoding = encoding, elapsed_time = stop - start)
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   101
      }
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
   102
    }
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
   103
73422
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73421
diff changeset
   104
    def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content =
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73421
diff changeset
   105
      get_content(open_connection(url, timeout = timeout, user_agent = user_agent))
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
   106
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   107
    def post(
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   108
      url: URL,
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   109
      parameters: List[(String, Any)],
73422
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73421
diff changeset
   110
      timeout: Time = default_timeout,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   111
      user_agent: String = ""
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   112
    ): Content = {
73422
fc7a0ea94c43 support timeout, similar to perl LWP::UserAgent;
wenzelm
parents: 73421
diff changeset
   113
      val connection = open_connection(url, timeout = timeout, user_agent = user_agent)
73421
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   114
      connection.setRequestMethod("POST")
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   115
      connection.setDoOutput(true)
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
   116
74094
6113f1db4342 clarified signature;
wenzelm
parents: 73716
diff changeset
   117
      val boundary = UUID.random().toString
73421
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   118
      connection.setRequestProperty(
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   119
        "Content-Type", "multipart/form-data; boundary=" + quote(boundary))
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
   120
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   121
      using(connection.getOutputStream) { out =>
73421
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   122
        def output(s: String): Unit = out.write(UTF8.bytes(s))
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   123
        def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE))
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   124
        def output_boundary(end: Boolean = false): Unit =
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   125
          output("--" + boundary + (if (end) "--" else "") + NEWLINE)
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   126
        def output_name(name: String): Unit =
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   127
          output("Content-Disposition: form-data; name=" + quote(name))
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   128
        def output_value(value: Any): Unit = {
73421
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   129
          output_newline(2)
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   130
          output(value.toString)
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   131
        }
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   132
        def output_content(content: Content): Unit = {
73421
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   133
          proper_string(content.file_name).foreach(s => output("; filename=" + quote(s)))
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   134
          output_newline()
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   135
          proper_string(content.mime_type).foreach(s => output("Content-Type: " + s))
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   136
          output_newline(2)
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   137
          content.bytes.write_stream(out)
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   138
        }
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
   139
73421
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   140
        output_newline(2)
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
   141
73421
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   142
        for { (name, value) <- parameters } {
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   143
          output_boundary()
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   144
          output_name(name)
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   145
          value match {
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   146
            case content: Content => output_content(content)
75106
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
   147
            case file: JFile => output_content(Content.read(file))
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
   148
            case path: Path => output_content(Content.read(path))
73421
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   149
            case _ => output_value(value)
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   150
          }
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   151
          output_newline()
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   152
        }
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   153
        output_boundary(end = true)
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   154
        out.flush()
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   155
      }
73417
1dcc2b228b8b clarified HTTP.Content: support encoding;
wenzelm
parents: 73416
diff changeset
   156
73421
a114ecd280ca clarified signature;
wenzelm
parents: 73417
diff changeset
   157
      get_content(connection)
73416
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
   158
    }
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
   159
  }
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
   160
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
   161
08aa4c1ed579 clarified signature: more explicit HTTP operations;
wenzelm
parents: 73413
diff changeset
   162
65081
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   163
  /** server **/
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   164
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   165
  /* request */
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   166
75108
05ba781cf890 clarified signature;
wenzelm
parents: 75107
diff changeset
   167
  def url_path(names: String*): String =
05ba781cf890 clarified signature;
wenzelm
parents: 75107
diff changeset
   168
    names.iterator.flatMap(a => if (a.isEmpty) None else Some("/" + a)).mkString
05ba781cf890 clarified signature;
wenzelm
parents: 75107
diff changeset
   169
05ba781cf890 clarified signature;
wenzelm
parents: 75107
diff changeset
   170
  class Request private[HTTP](
75146
1ef43607aef2 clarified signature;
wenzelm
parents: 75145
diff changeset
   171
    val server_name: String,
1ef43607aef2 clarified signature;
wenzelm
parents: 75145
diff changeset
   172
    val service_name: String,
75108
05ba781cf890 clarified signature;
wenzelm
parents: 75107
diff changeset
   173
    val uri: URI,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   174
    val input: Bytes
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   175
  ) {
75146
1ef43607aef2 clarified signature;
wenzelm
parents: 75145
diff changeset
   176
    def home: String = url_path(server_name, service_name)
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   177
    def root: String = home + "/"
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   178
    def query: String = home + "?"
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   179
75109
e6162afc5460 more robust toplevel url: allow extra "/";
wenzelm
parents: 75108
diff changeset
   180
    def toplevel: Boolean = uri_name == home || uri_name == root
e6162afc5460 more robust toplevel url: allow extra "/";
wenzelm
parents: 75108
diff changeset
   181
e6162afc5460 more robust toplevel url: allow extra "/";
wenzelm
parents: 75108
diff changeset
   182
    val uri_name: String = uri.toString
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   183
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   184
    def uri_path: Option[Path] =
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   185
      for {
75111
wenzelm
parents: 75110
diff changeset
   186
        s <- Option(uri.getPath).flatMap(Library.try_unprefix(root, _))
wenzelm
parents: 75110
diff changeset
   187
        if Path.is_wellformed(s)
wenzelm
parents: 75110
diff changeset
   188
        p = Path.explode(s) if p.all_basic
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   189
      } yield p
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   190
75112
899e70a9af83 tuned signature;
wenzelm
parents: 75111
diff changeset
   191
    def decode_query: Option[String] =
899e70a9af83 tuned signature;
wenzelm
parents: 75111
diff changeset
   192
      Library.try_unprefix(query, uri_name).map(Url.decode)
899e70a9af83 tuned signature;
wenzelm
parents: 75111
diff changeset
   193
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   194
    def decode_properties: Properties.T =
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   195
      space_explode('&', input.text).map(
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   196
        {
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   197
          case Properties.Eq(a, b) => Url.decode(a) -> Url.decode(b)
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   198
          case s => error("Malformed key-value pair in HTTP/POST: " + quote(s))
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   199
        })
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   200
  }
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   201
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   202
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   203
  /* response */
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   204
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   205
  object Response {
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   206
    def apply(
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   207
        bytes: Bytes = Bytes.empty,
75106
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
   208
        content_type: String = Content.mime_type_bytes): Response =
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   209
      new Response(bytes, content_type)
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   210
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   211
    val empty: Response = apply()
75106
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
   212
    def text(s: String): Response = apply(Bytes(s), Content.mime_type_text)
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
   213
    def html(s: String): Response = apply(Bytes(s), Content.mime_type_html)
75105
03115c9eea00 support for PDF.js: platform-independent PDF viewer;
wenzelm
parents: 75104
diff changeset
   214
03115c9eea00 support for PDF.js: platform-independent PDF viewer;
wenzelm
parents: 75104
diff changeset
   215
    def content(content: Content): Response = apply(content.bytes, content.mime_type)
75106
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
   216
    def read(file: JFile): Response = content(Content.read(file))
c2570d25d512 clarified signature;
wenzelm
parents: 75105
diff changeset
   217
    def read(path: Path): Response = content(Content.read(path))
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   218
  }
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   219
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   220
  class Response private[HTTP](val output: Bytes, val content_type: String) {
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   221
    override def toString: String = output.toString
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   222
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   223
    def write(http: HttpExchange, code: Int): Unit = {
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   224
      http.getResponseHeaders.set("Content-Type", content_type)
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   225
      http.sendResponseHeaders(code, output.length.toLong)
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   226
      using(http.getResponseBody)(output.write_stream)
65078
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   227
    }
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   228
  }
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   229
2339994e8790 more operations;
wenzelm
parents: 65077
diff changeset
   230
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   231
  /* service */
66207
8d5cb4ea2b7c support for HTTP/POST method;
wenzelm
parents: 65999
diff changeset
   232
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   233
  abstract class Service(val name: String, method: String = "GET") {
75146
1ef43607aef2 clarified signature;
wenzelm
parents: 75145
diff changeset
   234
    override def toString: String = name
75113
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   235
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   236
    def apply(request: Request): Option[Response]
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   237
75146
1ef43607aef2 clarified signature;
wenzelm
parents: 75145
diff changeset
   238
    def context(server_name: String): String =
1ef43607aef2 clarified signature;
wenzelm
parents: 75145
diff changeset
   239
      proper_string(url_path(server_name, name)).getOrElse("/")
75113
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   240
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   241
    def handler(server_name: String): HttpHandler = { (http: HttpExchange) =>
75113
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   242
      val uri = http.getRequestURI
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   243
      val input = using(http.getRequestBody)(Bytes.read_stream(_))
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   244
      if (http.getRequestMethod == method) {
75146
1ef43607aef2 clarified signature;
wenzelm
parents: 75145
diff changeset
   245
        val request = new Request(server_name, name, uri, input)
75113
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   246
        Exn.capture(apply(request)) match {
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   247
          case Exn.Res(Some(response)) =>
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   248
            response.write(http, 200)
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   249
          case Exn.Res(None) =>
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   250
            Response.empty.write(http, 404)
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   251
          case Exn.Exn(ERROR(msg)) =>
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   252
            Response.text(Output.error_message_text(msg)).write(http, 500)
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   253
          case Exn.Exn(exn) => throw exn
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   254
        }
75113
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   255
      }
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   256
      else Response.empty.write(http, 400)
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   257
    }
73413
56c0a793cd8b clarified signature;
wenzelm
parents: 73367
diff changeset
   258
  }
66207
8d5cb4ea2b7c support for HTTP/POST method;
wenzelm
parents: 65999
diff changeset
   259
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   260
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   261
  /* server */
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   262
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   263
  class Server private[HTTP](val name: String, val http_server: HttpServer) {
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   264
    def += (service: Service): Unit =
75108
05ba781cf890 clarified signature;
wenzelm
parents: 75107
diff changeset
   265
      http_server.createContext(service.context(name), service.handler(name))
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   266
    def -= (service: Service): Unit =
75108
05ba781cf890 clarified signature;
wenzelm
parents: 75107
diff changeset
   267
      http_server.removeContext(service.context(name))
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   268
73439
cb127ce2c092 tuned --- following hints by IntelliJ;
wenzelm
parents: 73438
diff changeset
   269
    def start(): Unit = http_server.start()
73367
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   270
    def stop(): Unit = http_server.stop(0)
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   271
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   272
    def address: InetSocketAddress = http_server.getAddress
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   273
75108
05ba781cf890 clarified signature;
wenzelm
parents: 75107
diff changeset
   274
    def url: String = "http://" + address.getHostName + ":" + address.getPort + url_path(name)
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   275
    override def toString: String = url
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   276
  }
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   277
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   278
  def server(
76270
d3fce4feb142 clarified signature: more arguments;
wenzelm
parents: 75394
diff changeset
   279
    port: Int = 0,
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   280
    name: String = UUID.random().toString,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   281
    services: List[Service] = isabelle_services
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   282
  ): Server = {
76270
d3fce4feb142 clarified signature: more arguments;
wenzelm
parents: 75394
diff changeset
   283
    val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, port), 0)
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   284
    http_server.setExecutor(null)
65076
8a96ab58f016 clarified signature;
wenzelm
parents: 63823
diff changeset
   285
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   286
    val server = new Server(name, http_server)
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   287
    for (service <- services) server += service
65077
2d6e716c9d6e clarified modules;
wenzelm
parents: 65076
diff changeset
   288
    server
63823
ca8b737b08cf minimal HTTP server;
wenzelm
parents:
diff changeset
   289
  }
65079
8a5c2b86c5f6 handler for Isabelle fonts;
wenzelm
parents: 65078
diff changeset
   290
8a5c2b86c5f6 handler for Isabelle fonts;
wenzelm
parents: 65078
diff changeset
   291
65081
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   292
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   293
  /** Isabelle services **/
65081
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   294
75113
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   295
  def isabelle_services: List[Service] =
75145
e721880779be clarified signature;
wenzelm
parents: 75121
diff changeset
   296
    List(Welcome_Service, Fonts_Service, PDFjs_Service, Docs_Service)
65081
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   297
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   298
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   299
  /* welcome */
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   300
75145
e721880779be clarified signature;
wenzelm
parents: 75121
diff changeset
   301
  object Welcome_Service extends Welcome()
e721880779be clarified signature;
wenzelm
parents: 75121
diff changeset
   302
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   303
  class Welcome(name: String = "") extends Service(name) {
75113
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   304
    def apply(request: Request): Option[Response] =
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   305
      if (request.toplevel) {
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   306
        Some(Response.text("Welcome to " + Isabelle_System.identification()))
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   307
      }
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   308
      else None
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   309
  }
65081
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   310
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   311
c20905a5bc8e handler for Isabelle version;
wenzelm
parents: 65080
diff changeset
   312
  /* fonts */
65079
8a5c2b86c5f6 handler for Isabelle fonts;
wenzelm
parents: 65078
diff changeset
   313
75145
e721880779be clarified signature;
wenzelm
parents: 75121
diff changeset
   314
  object Fonts_Service extends Fonts()
e721880779be clarified signature;
wenzelm
parents: 75121
diff changeset
   315
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   316
  class Fonts(name: String = "fonts") extends Service(name) {
75113
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   317
    private lazy val html_fonts: List[Isabelle_Fonts.Entry] =
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   318
      Isabelle_Fonts.fonts(hidden = true)
65079
8a5c2b86c5f6 handler for Isabelle fonts;
wenzelm
parents: 65078
diff changeset
   319
75113
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   320
    def apply(request: Request): Option[Response] =
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   321
      if (request.toplevel) {
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   322
        Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name))))
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   323
      }
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   324
      else {
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   325
        request.uri_path.flatMap(path =>
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   326
          html_fonts.collectFirst(
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   327
            { case entry if path == entry.path.base => Response(entry.bytes) }
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   328
          ))
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   329
      }
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   330
  }
75105
03115c9eea00 support for PDF.js: platform-independent PDF viewer;
wenzelm
parents: 75104
diff changeset
   331
03115c9eea00 support for PDF.js: platform-independent PDF viewer;
wenzelm
parents: 75104
diff changeset
   332
03115c9eea00 support for PDF.js: platform-independent PDF viewer;
wenzelm
parents: 75104
diff changeset
   333
  /* pdfjs */
03115c9eea00 support for PDF.js: platform-independent PDF viewer;
wenzelm
parents: 75104
diff changeset
   334
75145
e721880779be clarified signature;
wenzelm
parents: 75121
diff changeset
   335
  object PDFjs_Service extends PDFjs()
e721880779be clarified signature;
wenzelm
parents: 75121
diff changeset
   336
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   337
  class PDFjs(name: String = "pdfjs") extends Service(name) {
75113
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   338
    def apply(request: Request): Option[Response] =
75105
03115c9eea00 support for PDF.js: platform-independent PDF viewer;
wenzelm
parents: 75104
diff changeset
   339
      for {
75107
7c0217c8b8a5 clarified signature;
wenzelm
parents: 75106
diff changeset
   340
        p <- request.uri_path
75117
4b3ae1a3bbbd more robust;
wenzelm
parents: 75113
diff changeset
   341
        path = Path.explode("$ISABELLE_PDFJS_HOME") + p if path.is_file
4b3ae1a3bbbd more robust;
wenzelm
parents: 75113
diff changeset
   342
        s = p.implode if s.startsWith("build/") || s.startsWith("web/")
75113
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   343
      } yield Response.read(path)
a7a489ea4661 clarified signature;
wenzelm
parents: 75112
diff changeset
   344
  }
75119
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   345
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   346
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   347
  /* docs */
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   348
75145
e721880779be clarified signature;
wenzelm
parents: 75121
diff changeset
   349
  object Docs_Service extends Docs()
e721880779be clarified signature;
wenzelm
parents: 75121
diff changeset
   350
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75146
diff changeset
   351
  class Docs(name: String = "docs") extends PDFjs(name) {
75119
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   352
    private val doc_contents = isabelle.Doc.main_contents()
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   353
75121
2efbb4e813ad clarified URL;
wenzelm
parents: 75120
diff changeset
   354
    // example: .../docs/web/viewer.html?file=system.pdf
75119
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   355
    def doc_request(request: Request): Option[Response] =
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   356
      for {
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   357
        p <- request.uri_path if p.is_pdf
75121
2efbb4e813ad clarified URL;
wenzelm
parents: 75120
diff changeset
   358
        s = p.implode if s.startsWith("web/")
75119
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   359
        name = p.base.split_ext._1.implode
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   360
        doc <- doc_contents.docs.find(_.name == name)
75120
488c7e8923b2 clarified pdf path;
wenzelm
parents: 75119
diff changeset
   361
      } yield Response.read(doc.path)
75119
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   362
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   363
    override def apply(request: Request): Option[Response] =
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   364
      doc_request(request) orElse super.apply(request)
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   365
  }
7bf685cbc789 HTTP view of Isabelle PDF documentation;
wenzelm
parents: 75117
diff changeset
   366
}