src/Pure/General/http.scala

tuned output syntax: INV and VAR are now blocks

/*  Title:      Pure/General/http.scala
    Author:     Makarius

HTTP client and server support.
*/

package isabelle


import java.io.{File => JFile}
import java.net.{InetSocketAddress, URI, URL, URLConnection, HttpURLConnection}
import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}


object HTTP
{
  /** content **/

  val mime_type_bytes: String = "application/octet-stream"
  val mime_type_text: String = "text/plain; charset=utf-8"
  val mime_type_html: String = "text/html; charset=utf-8"

  val default_mime_type: String = mime_type_bytes
  val default_encoding: String = UTF8.charset_name

  sealed case class Content(
    bytes: Bytes,
    file_name: String = "",
    mime_type: String = default_mime_type,
    encoding: String = default_encoding,
    elapsed_time: Time = Time.zero)
  {
    def text: String = new String(bytes.array, encoding)
    def json: JSON.T = JSON.parse(text)
  }

  def read_content(file: JFile): Content =
  {
    val bytes = Bytes.read(file)
    val file_name = file.getName
    val mime_type =
      Option(URLConnection.guessContentTypeFromName(file_name)).getOrElse(default_mime_type)
    Content(bytes, file_name = file_name, mime_type = mime_type)
  }

  def read_content(path: Path): Content = read_content(path.file)



  /** client **/

  val NEWLINE: String = "\r\n"

  object Client
  {
    val default_timeout: Time = Time.seconds(180)

    def open_connection(url: URL,
      timeout: Time = default_timeout,
      user_agent: String = ""): HttpURLConnection =
    {
      url.openConnection match {
        case connection: HttpURLConnection =>
          if (0 < timeout.ms && timeout.ms <= Integer.MAX_VALUE) {
            val ms = timeout.ms.toInt
            connection.setConnectTimeout(ms)
            connection.setReadTimeout(ms)
          }
          proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s))
          connection
        case _ => error("Bad URL (not HTTP): " + quote(url.toString))
      }
    }

    def get_content(connection: HttpURLConnection): Content =
    {
      val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r

      val start = Time.now()
      using(connection.getInputStream)(stream =>
      {
        val bytes = Bytes.read_stream(stream, hint = connection.getContentLength)
        val stop = Time.now()

        val file_name = Url.file_name(connection.getURL)
        val mime_type = Option(connection.getContentType).getOrElse(default_mime_type)
        val encoding =
          (connection.getContentEncoding, mime_type) match {
            case (enc, _) if enc != null => enc
            case (_, Charset(enc)) => enc
            case _ => default_encoding
          }
        Content(bytes, file_name = file_name, mime_type = mime_type,
          encoding = encoding, elapsed_time = stop - start)
      })
    }

    def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content =
      get_content(open_connection(url, timeout = timeout, user_agent = user_agent))

    def post(url: URL, parameters: List[(String, Any)],
      timeout: Time = default_timeout,
      user_agent: String = ""): Content =
    {
      val connection = open_connection(url, timeout = timeout, user_agent = user_agent)
      connection.setRequestMethod("POST")
      connection.setDoOutput(true)

      val boundary = UUID.random().toString
      connection.setRequestProperty(
        "Content-Type", "multipart/form-data; boundary=" + quote(boundary))

      using(connection.getOutputStream)(out =>
      {
        def output(s: String): Unit = out.write(UTF8.bytes(s))
        def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE))
        def output_boundary(end: Boolean = false): Unit =
          output("--" + boundary + (if (end) "--" else "") + NEWLINE)
        def output_name(name: String): Unit =
          output("Content-Disposition: form-data; name=" + quote(name))
        def output_value(value: Any): Unit =
        {
          output_newline(2)
          output(value.toString)
        }
        def output_content(content: Content): Unit =
        {
          proper_string(content.file_name).foreach(s => output("; filename=" + quote(s)))
          output_newline()
          proper_string(content.mime_type).foreach(s => output("Content-Type: " + s))
          output_newline(2)
          content.bytes.write_stream(out)
        }

        output_newline(2)

        for { (name, value) <- parameters } {
          output_boundary()
          output_name(name)
          value match {
            case content: Content => output_content(content)
            case file: JFile => output_content(read_content(file))
            case path: Path => output_content(read_content(path))
            case _ => output_value(value)
          }
          output_newline()
        }
        output_boundary(end = true)
        out.flush()
      })

      get_content(connection)
    }
  }



  /** server **/

  /* response */

  object Response
  {
    def apply(
        bytes: Bytes = Bytes.empty,
        content_type: String = mime_type_bytes): Response =
      new Response(bytes, content_type)

    val empty: Response = apply()
    def text(s: String): Response = apply(Bytes(s), mime_type_text)
    def html(s: String): Response = apply(Bytes(s), mime_type_html)
  }

  class Response private[HTTP](val bytes: Bytes, val content_type: String)
  {
    override def toString: String = bytes.toString
  }


  /* exchange */

  class Exchange private[HTTP](val http_exchange: HttpExchange)
  {
    def request_method: String = http_exchange.getRequestMethod
    def request_uri: URI = http_exchange.getRequestURI

    def read_request(): Bytes =
      using(http_exchange.getRequestBody)(Bytes.read_stream(_))

    def write_response(code: Int, response: Response): Unit =
    {
      http_exchange.getResponseHeaders.set("Content-Type", response.content_type)
      http_exchange.sendResponseHeaders(code, response.bytes.length.toLong)
      using(http_exchange.getResponseBody)(response.bytes.write_stream)
    }
  }


  /* handler for request method */

  sealed case class Arg(method: String, uri: URI, request: Bytes)
  {
    def decode_properties: Properties.T =
      space_explode('&', request.text).map(
        {
          case Properties.Eq(a, b) => Url.decode(a) -> Url.decode(b)
          case s => error("Malformed key-value pair in HTTP/POST: " + quote(s))
        })
  }

  object Handler
  {
    def apply(root: String, body: Exchange => Unit): Handler =
      new Handler(root, (x: HttpExchange) => body(new Exchange(x)))

    def method(name: String, root: String, body: Arg => Option[Response]): Handler =
      apply(root, http =>
        {
          val request = http.read_request()
          if (http.request_method == name) {
            val arg = Arg(name, http.request_uri, request)
            Exn.capture(body(arg)) match {
              case Exn.Res(Some(response)) =>
                http.write_response(200, response)
              case Exn.Res(None) =>
                http.write_response(404, Response.empty)
              case Exn.Exn(ERROR(msg)) =>
                http.write_response(500, Response.text(Output.error_message_text(msg)))
              case Exn.Exn(exn) => throw exn
            }
          }
          else http.write_response(400, Response.empty)
        })

    def get(root: String, body: Arg => Option[Response]): Handler = method("GET", root, body)
    def post(root: String, body: Arg => Option[Response]): Handler = method("POST", root, body)
  }

  class Handler private(val root: String, val handler: HttpHandler)
  {
    override def toString: String = root
  }


  /* server */

  class Server private[HTTP](val http_server: HttpServer)
  {
    def += (handler: Handler): Unit = http_server.createContext(handler.root, handler.handler)
    def -= (handler: Handler): Unit = http_server.removeContext(handler.root)

    def start(): Unit = http_server.start()
    def stop(): Unit = http_server.stop(0)

    def address: InetSocketAddress = http_server.getAddress
    def url: String = "http://" + address.getHostName + ":" + address.getPort
    override def toString: String = url
  }

  def server(handlers: List[Handler] = isabelle_resources): Server =
  {
    val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0)
    http_server.setExecutor(null)

    val server = new Server(http_server)
    for (handler <- handlers) server += handler
    server
  }



  /** Isabelle resources **/

  lazy val isabelle_resources: List[Handler] =
    List(welcome(), fonts())


  /* welcome */

  def welcome(root: String = "/"): Handler =
    Handler.get(root, arg =>
      if (arg.uri.toString == root) {
        Some(Response.text("Welcome to " + Isabelle_System.identification()))
      }
      else None)


  /* fonts */

  private lazy val html_fonts: List[Isabelle_Fonts.Entry] =
    Isabelle_Fonts.fonts(hidden = true)

  def fonts(root: String = "/fonts"): Handler =
    Handler.get(root, arg =>
      {
        val uri_name = arg.uri.toString
        if (uri_name == root) {
          Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name))))
        }
        else {
          html_fonts.collectFirst(
            { case entry if uri_name == root + "/" + entry.path.file_name => Response(entry.bytes) })
        }
      })
}