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