# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1711757305 -3600
# Node ID 37ea0727291f1b214fb7a44e5240ecc66cf18d63
# Parent  68f6b29ae06692ff5b5287583cefb35e21d65851
moved web_app module from AFP (e.g., for building web services for the distributed build);

diff -r 68f6b29ae066 -r 37ea0727291f etc/build.props
--- a/etc/build.props	Thu Mar 28 15:08:58 2024 +0100
+++ b/etc/build.props	Sat Mar 30 01:08:25 2024 +0100
@@ -200,6 +200,7 @@
   src/Pure/System/setup_tool.scala \
   src/Pure/System/system_channel.scala \
   src/Pure/System/tty_loop.scala \
+  src/Pure/System/web_app.scala \
   src/Pure/Thy/document_build.scala \
   src/Pure/Thy/thy_element.scala \
   src/Pure/Thy/thy_header.scala \
diff -r 68f6b29ae066 -r 37ea0727291f src/Pure/System/web_app.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/web_app.scala	Sat Mar 30 01:08:25 2024 +0100
@@ -0,0 +1,496 @@
+/*  Title:      Pure/System/web_app.scala
+    Author:     Fabian Huch, TU Muenchen
+
+Technical layer for web apps using server-side rendering with HTML forms.
+ */
+package isabelle
+
+
+import scala.annotation.tailrec
+import scala.collection.immutable.SortedMap
+
+
+object Web_App {
+  /* form html elements */
+
+  object More_HTML {
+    import HTML._
+
+    def css(s: String): Attribute = new Attribute("style", s)
+    def name(n: String): Attribute = new Attribute("name", n)
+    def value(v: String): Attribute = new Attribute("value", v)
+    def placeholder(p: String): Attribute = new Attribute("placeholder", p)
+
+    val fieldset = new Operator("fieldset")
+    val button = new Operator("button")
+
+    def legend(txt: String): XML.Elem = XML.Elem(Markup("legend", Nil), text(txt))
+    def input(typ: String): XML.Elem = XML.Elem(Markup("input", List("type" -> typ)), Nil)
+    def hidden(k: Params.Key, v: String): XML.Elem =
+      id(k.print)(name(k.print)(value(v)(input("hidden"))))
+
+    def textfield(i: Params.Key, p: String, v: String): XML.Elem =
+      id(i.print)(name(i.print)(value(v)(placeholder(p)(input("text")))))
+
+    def browse(i: Params.Key, accept: List[String]): XML.Elem =
+      id(i.print)(name(i.print)(input("file"))) + ("accept" -> accept.mkString(","))
+
+    def label(`for`: Params.Key, txt: String): XML.Elem =
+      XML.Elem(Markup("label", List("for" -> `for`.print)), text(txt))
+
+    def option(k: String, v: String): XML.Elem = value(k)(XML.elem("option", text(v)))
+
+    def optgroup(txt: String, opts: XML.Body): XML.Elem =
+      XML.Elem(Markup("optgroup", List("label" -> txt)), opts)
+
+    def select(i: Params.Key, opts: XML.Body): XML.Elem =
+      id(i.print)(name(i.print)(XML.elem("select", opts)))
+
+    def textarea(i: Params.Key, v: String): XML.Elem =
+      id(i.print)(name(i.print)(value(v)(XML.elem("textarea", text(v + "\n")))))
+
+    def radio(i: Params.Key, v: Params.Key, values: List[(Params.Key, String)]): XML.Elem = {
+      def to_option(k: Params.Key): XML.Elem = {
+        val elem = id(i.print + k)(name(i.print)(value(k.print)(input("radio"))))
+        if (v == k) elem + ("checked" -> "checked") else elem
+      }
+
+      span(values.map { case (k, v) => span(List(label(i + k, v), to_option(k))) })
+    }
+
+    def selection(i: Params.Key, selected: Option[String], opts: XML.Body): XML.Elem = {
+      def sel(elem: XML.Tree): XML.Tree = {
+        selected match {
+          case Some(value) =>
+            val Value = new Properties.String("value")
+            elem match {
+              case XML.Elem(Markup("optgroup", props), body) =>
+                XML.Elem(Markup("optgroup", props), body.map(sel))
+              case e@XML.Elem(Markup("option", Value(v)), _) if v == value =>
+                e + ("selected" -> "selected")
+              case e => e
+            }
+          case None => elem
+        }
+      }
+
+      def is_empty_group(elem: XML.Tree): Boolean = elem match {
+        case XML.Elem(Markup("optgroup", _), body) if body.isEmpty => true
+        case _ => false
+      }
+
+      val default = if (selected.isEmpty) List(option("", "") + ("hidden" -> "hidden")) else Nil
+      select(i, default ::: opts.filterNot(is_empty_group).map(sel))
+    }
+
+    def api_button(call: String, label: String): XML.Elem =
+      button(text(label)) + ("formaction" -> call) + ("type" -> "submit")
+
+    def submit_form(endpoint: String, body: XML.Body): XML.Elem = {
+      val default_button = css("display: none")(input("submit") + ("formaction" -> endpoint))
+      val attrs =
+        List("method" -> "post", "target" -> "iframe", "enctype" -> "multipart/form-data")
+      XML.Elem(Markup("form", attrs), default_button :: body)
+    }
+  }
+
+
+  /* form http handling */
+
+  object Multi_Part {
+    abstract class Data(name: String)
+    case class Param(name: String, value: String) extends Data(name)
+    case class File(name: String, file_name: String, content: Bytes) extends Data(name)
+
+    def parse(body: Bytes): List[Data] = {
+      /* Seq for text with embedded bytes */
+      case class Seq(text: String, bytes: Bytes) {
+        def split_one(sep: String): Option[(Seq, Seq)] = {
+          val text_i = text.indexOf(sep)
+          if (text_i >= 0 && sep.nonEmpty) {
+            val (before_text, at_text) = text.splitAt(text_i)
+            val after_text = at_text.substring(sep.length)
+
+            // text might be shorter than bytes because of misinterpreted characters
+            var found = false
+            var bytes_i = 0
+            while (!found && bytes_i < bytes.length) {
+              var sep_ok = true
+              var sep_i = 0
+              while (sep_ok && sep_i < sep.length) {
+                if (bytes.charAt(bytes_i + sep_i) == sep.charAt(sep_i)) {
+                  sep_i += 1
+                } else {
+                  bytes_i += 1
+                  sep_ok = false
+                }
+              }
+              if (sep_ok) found = true
+            }
+
+            val before_bytes = bytes.subSequence(0, bytes_i)
+            val after_bytes = bytes.subSequence(bytes_i + sep.length, bytes.length)
+
+            Some(Seq(before_text, before_bytes), Seq(after_text, after_bytes))
+          } else None
+        }
+      }
+
+      val s = Seq(body.text, body)
+
+      def perhaps_unprefix(pfx: String, s: Seq): Seq =
+        Library.try_unprefix(pfx, s.text) match {
+          case Some(text) => Seq(text, s.bytes.subSequence(pfx.length, s.bytes.length))
+          case None => s
+        }
+
+      val Separator = """--(.*)""".r
+
+      s.split_one(HTTP.NEWLINE) match {
+        case Some(Seq(Separator(sep), _), rest) =>
+          val Param = """Content-Disposition: form-data; name="([^"]+)"""".r
+          val File = """Content-Disposition: form-data; name="([^"]+)"; filename="([^"]+)"""".r
+
+          def parts(body: Seq): Option[List[Data]] =
+            for {
+              (first_line, more) <- body.split_one(HTTP.NEWLINE)
+              more1 = perhaps_unprefix(HTTP.NEWLINE, more)
+              (value, rest) <- more1.split_one(HTTP.NEWLINE + "--" + sep)
+              rest1 = perhaps_unprefix(HTTP.NEWLINE, rest)
+            } yield first_line.text match {
+              case Param(name) =>
+                Multi_Part.Param(name, Line.normalize(value.text)) :: parts(rest1).getOrElse(Nil)
+              case File(name, file_name) =>
+                value.split_one(HTTP.NEWLINE + HTTP.NEWLINE) match {
+                  case Some(_, content) =>
+                    Multi_Part.File(name, file_name, content.bytes) :: parts(rest1).getOrElse(Nil)
+                  case _ => parts(rest1).getOrElse(Nil)
+                }
+              case _ => Nil
+            }
+
+          parts(rest).getOrElse(Nil)
+        case _ => Nil
+      }
+    }
+  }
+
+
+  /* request parameters as structured data */
+
+  object Params {
+    def key(elems: (String | Int)*): Key =
+      Key(
+        elems.toList.map {
+          case s: String => Key.elem(s)
+          case i: Int => Key.elem(i)
+        })
+
+    object Key {
+      sealed trait Elem { def print: String }
+
+      class Nested_Elem private[Key](val rep: String) extends Elem {
+        override def equals(that: Any): Boolean =
+          that match {
+            case other: Nested_Elem => rep == other.rep
+            case _ => false
+          }
+        override def hashCode(): Int = rep.hashCode
+
+        def print: String = rep
+        override def toString: String = print
+      }
+
+      class List_Elem private[Key](val rep: Int) extends Elem {
+        override def equals(that: Any): Boolean =
+          that match {
+            case other: List_Elem => rep == other.rep
+            case _ => false
+          }
+        override def hashCode(): Int = rep.hashCode
+
+        def print: String = rep.toString
+        override def toString: String = print
+      }
+
+      def elem(s: String): Nested_Elem =
+        if (!s.forall(Symbol.is_ascii_letter)) error("Illegal element in: " + quote(s))
+        else new Nested_Elem(s)
+
+      def elem(i: Int): List_Elem =
+        if (i < 0) error("Illegal list element") else new List_Elem(i)
+
+      def empty: Key = Key(Nil)
+      def apply(s: String): Key = new Key(List(elem(s)))
+      def explode(s: String): Key =
+        new Key(
+          space_explode('_', s).map {
+            case Value.Int(i) => elem(i)
+            case s => elem(s)
+          })
+
+
+      /* ordering */
+
+      object Ordering extends scala.math.Ordering[Key] {
+        def compare(key1: Key, key2: Key): Int = key1.print.compareTo(key2.print)
+      }
+    }
+
+    case class Key(rep: List[Key.Elem]) {
+      def +(elem: Key.Elem): Key = Key(rep :+ elem)
+      def +(i: Int): Key = this + Key.elem(i)
+      def +(s: String): Key = this + Key.elem(s)
+      def +(key: Key) = Key(rep ++ key.rep)
+
+      def num: Option[Int] =
+        rep match {
+          case (e: Key.List_Elem) :: _ => Some(e.rep)
+          case _ => None
+        }
+
+      def get(key: Key): Option[Key] =
+        if (rep.startsWith(key.rep)) Some(Key(rep.drop(key.rep.length))) else None
+
+      def print = rep.map(_.print).mkString("_")
+      override def toString: String = print
+    }
+
+    def indexed[A, B](key: Key, xs: List[A], f: (Key, A) => B): List[B] =
+      for ((x, i) <- xs.zipWithIndex) yield f(key + i, x)
+
+
+    object Data {
+      def from_multipart(parts: List[Multi_Part.Data]): Data = {
+        val files = parts.collect { case f: Multi_Part.File => f }
+        val params =
+          parts.collect { case Multi_Part.Param(name, value) => Key.explode(name) -> value }
+        val file_params = files.map(file => Key.explode(file.name) -> file.file_name)
+        val file_files = files.map(file => Key.explode(file.name) -> file.content)
+
+        new Data(
+          SortedMap.from(params ++ file_params)(Key.Ordering),
+          SortedMap.from(file_files)(Key.Ordering))
+      }
+    }
+
+    class Data private(params: SortedMap[Key, String], files: SortedMap[Key, Bytes]) {
+      override def toString: String = "Data(" + params.toString() + "," + files.toString() + ")"
+
+      def get(key: Key): Option[String] = params.get(key)
+      def apply(key: Key): String = get(key).getOrElse("")
+      def list(key: Key): List[Key] =
+        (for {
+          key1 <- params.keys.toList
+          key2 <- key1.get(key)
+          i <- key2.num
+        } yield key + i).distinct
+
+      def file(key: Key): Option[Bytes] = files.get(key)
+    }
+  }
+
+
+  /* API with backend base path, and application url (e.g. for frontend links). */
+
+  case class Paths(
+    frontend: Url,
+    api_base: Path,
+    serve_frontend: Boolean = false,
+    landing: Path = Path.current
+  ) {
+    def api_path(path: Path, external: Boolean = true): Path =
+      (if (serve_frontend) Path.explode("backend") else Path.current) +
+        (if (external) api_base else Path.current) + path
+
+    def route(path: Path, params: Properties.T = Nil): String = {
+      def param(p: Properties.Entry): String = Url.encode(p._1) + "=" + Url.encode(p._2)
+      val route =
+        if (params.isEmpty) path.implode else path.implode + "?" + params.map(param).mkString("&")
+      "/" + route
+    }
+
+    def api_route(path: Path, params: Properties.T = Nil, external: Boolean = true): String =
+      route(api_path(path, external = external), params)
+
+    def frontend_url(path: Path, params: Properties.T = Nil): Url =
+      frontend.resolve(route(path, params))
+  }
+
+  abstract class Server[A](
+    paths: Paths,
+    port: Int = 0,
+    verbose: Boolean = false,
+    progress: Progress = new Progress(),
+  ) {
+    def render(model: A): XML.Body
+    val error_model: A
+    val endpoints: List[Endpoint]
+    val head: XML.Body
+
+    def output_document(content: XML.Body, post_height: Boolean = true): String = {
+      val attrs =
+        if (post_height) List("onLoad" -> "parent.postMessage(document.body.scrollHeight, '*')")
+        else Nil
+
+      cat_lines(
+        List(
+          HTML.header,
+          HTML.output(XML.elem("head", HTML.head_meta :: head), hidden = true, structural = true),
+          HTML.output(XML.Elem(Markup("body", attrs), content), hidden = true, structural = true),
+          HTML.footer))
+    }
+
+    class UI(path: Path) extends HTTP.Service(path.implode, "GET") {
+      def apply(request: HTTP.Request): Option[HTTP.Response] = {
+        progress.echo_if(verbose, "GET ui")
+
+        val on_load = """
+(function() {
+  window.addEventListener('message', (event) => {
+    if (Number.isInteger(event.data)) {
+      this.style.height=event.data + 32 + 'px'
+    }
+  })
+}).call(this)"""
+
+        val set_src = """
+const base = '""" + paths.frontend.toString.replace("/", "\\/") + """'
+document.getElementById('iframe').src = base + '""" + paths.api_route(path).replace("/", "\\/") + """' + window.location.search"""
+
+        Some(HTTP.Response.html(output_document(
+          List(
+            XML.Elem(
+              Markup(
+                "iframe",
+                List(
+                  "id" -> "iframe",
+                  "name" -> "iframe",
+                  "style" -> "border-style: none; width: 100%",
+                  "onload" -> on_load)),
+              HTML.text("content")),
+            HTML.script(set_src)),
+            post_height = false)))
+      }
+    }
+
+    sealed abstract class Endpoint(path: Path, method: String = "GET")
+      extends HTTP.Service(paths.api_path(path, external = false).implode, method) {
+
+      def reply(request: HTTP.Request): HTTP.Response
+
+      final def apply(request: HTTP.Request): Option[HTTP.Response] =
+        Exn.capture(reply(request)) match {
+          case Exn.Res(res) => Some(res)
+          case Exn.Exn(exn) =>
+            val id = UUID.random_string()
+            progress.echo_error_message("Internal error <" + id + ">: " + exn)
+            error("Internal server error. ID: " + id)
+        }
+    }
+
+    private def query_params(request: HTTP.Request): Properties.T = {
+      def decode(s: String): Option[Properties.Entry] =
+        s match {
+          case Properties.Eq(k, v) => Some(Url.decode(k) -> Url.decode(v))
+          case _ => None
+        }
+
+      Library.try_unprefix(request.query, request.uri_name).toList.flatMap(params =>
+        space_explode('&', params).flatMap(decode))
+    }
+
+
+    /* endpoint types */
+
+    class Get(val path: Path, description: String, get: Properties.T => Option[A])
+      extends Endpoint(path) {
+
+      def reply(request: HTTP.Request): HTTP.Response = {
+        progress.echo_if(verbose, "GET " + description)
+
+        val params = query_params(request)
+        progress.echo_if(verbose, "params: " + params.toString())
+
+        val model =
+          get(params) match {
+            case Some(model) => model
+            case None =>
+              progress.echo_if(verbose, "Parsing failed")
+              error_model
+          }
+        HTTP.Response.html(output_document(render(model)))
+      }
+    }
+
+    class Get_File(path: Path, description: String, download: Properties.T => Option[Path])
+      extends Endpoint(path) {
+
+      def reply(request: HTTP.Request): HTTP.Response = {
+        progress.echo_if(verbose, "DOWNLOAD " + description)
+
+        val params = query_params(request)
+        progress.echo_if(verbose, "params: " + params.toString())
+
+        download(params) match {
+          case Some(path) => HTTP.Response.content(HTTP.Content.read(path))
+          case None =>
+            progress.echo_if(verbose, "Fetching file path failed")
+            HTTP.Response.html(output_document(render(error_model)))
+        }
+      }
+    }
+
+    class Post(path: Path, description: String, post: Params.Data => Option[A])
+      extends Endpoint(path, method = "POST") {
+
+      def reply(request: HTTP.Request): HTTP.Response = {
+        progress.echo_if(verbose, "POST " + description)
+
+        val parts = Multi_Part.parse(request.input)
+        val params = Params.Data.from_multipart(parts)
+        progress.echo_if(verbose, "params: " + params.toString)
+
+        val model =
+          post(params) match {
+            case Some(model) => model
+            case None =>
+              progress.echo_if(verbose, "Parsing failed")
+              error_model
+          }
+        HTTP.Response.html(output_document(render(model)))
+      }
+    }
+
+
+    /* server */
+
+    private def ui_endpoints =
+      if (paths.serve_frontend) endpoints.collect { case page: Get => new UI(page.path) } else Nil
+
+    private lazy val server =
+      HTTP.server(port = port, name = "", services = endpoints ::: ui_endpoints)
+
+    def run(): Unit = {
+      start()
+
+      @tailrec
+      def loop(): Unit = {
+        Thread.sleep(Long.MaxValue)
+        loop()
+      }
+
+      Isabelle_Thread.interrupt_handler(_ => server.stop()) { loop() }
+    }
+
+    def start(): Unit = {
+      server.start()
+      progress.echo("Server started on " + paths.frontend_url(paths.landing))
+    }
+
+    def stop(): Unit = {
+      server.stop()
+      progress.echo("Server stopped")
+    }
+  }
+}
\ No newline at end of file