# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1716987336 -7200
# Node ID 81f2fbf3975de191abad68ae60a22af1f829699a
# Parent  ca9a402735b4c2d04ce00876093d00c0294d650d
clarified web app endpoints;

diff -r ca9a402735b4 -r 81f2fbf3975d src/Pure/System/web_app.scala
--- a/src/Pure/System/web_app.scala	Tue May 28 19:51:49 2024 +0200
+++ b/src/Pure/System/web_app.scala	Wed May 29 14:55:36 2024 +0200
@@ -336,24 +336,38 @@
   ) {
     def render(model: A): XML.Body
     val error_model: A
-    val endpoints: List[Endpoint]
+    val endpoints: List[API_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
+
+    /* public-facing endpoints */
+
+    sealed abstract class Endpoint(path: Path, method: String = "GET")
+      extends HTTP.Service(path.implode, method) {
+
+      def reply(request: HTTP.Request): HTTP.Response
 
-      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))
+      def html(head: XML.Elem, body: XML.Elem): HTTP.Response =
+        HTTP.Response.html(
+          cat_lines(
+            List(
+              HTML.header,
+              HTML.output(head, hidden = true, structural = true),
+              HTML.output(body, hidden = true, structural = true),
+              HTML.footer)))
+
+      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)
+        }
     }
 
-    class UI(path: Path) extends HTTP.Service(path.implode, "GET") {
-      def apply(request: HTTP.Request): Option[HTTP.Response] = {
+    class UI(path: Path) extends Endpoint(path, "GET") {
+      def reply(request: HTTP.Request): HTTP.Response = {
         progress.echo_if(verbose, "GET ui")
 
         val on_load = """
@@ -369,8 +383,9 @@
 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(
+        html(
+          XML.elem("head", HTML.head_meta :: head),
+          XML.Elem(Markup("body", List("style" -> "height: fit-content")), List(
             XML.Elem(
               Markup(
                 "iframe",
@@ -380,24 +395,19 @@
                   "style" -> "border-style: none; width: 100%",
                   "onload" -> on_load)),
               HTML.text("content")),
-            HTML.script(set_src)),
-            post_height = false)))
+            HTML.script(set_src))))
       }
     }
 
-    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
+    sealed abstract class API_Endpoint(path: Path, method: String = "GET")
+      extends Endpoint(paths.api_path(path, external = false), method) {
 
-      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)
-        }
+      def html_content(content: XML.Body): HTTP.Response =
+        html(
+          XML.elem("head", HTML.head_meta :: head),
+          XML.Elem(
+            Markup("body", List("onLoad" -> "parent.postMessage(document.body.scrollHeight, '*')")),
+            content))
     }
 
     private def query_params(request: HTTP.Request): Properties.T = {
@@ -415,7 +425,7 @@
     /* endpoint types */
 
     class Get(val path: Path, description: String, get: Properties.T => Option[A])
-      extends Endpoint(path) {
+      extends API_Endpoint(path) {
 
       def reply(request: HTTP.Request): HTTP.Response = {
         progress.echo_if(verbose, "GET " + description)
@@ -430,12 +440,13 @@
               progress.echo_if(verbose, "Parsing failed")
               error_model
           }
-        HTTP.Response.html(output_document(render(model)))
+
+        html_content(render(model))
       }
     }
 
     class Get_File(path: Path, description: String, download: Properties.T => Option[Path])
-      extends Endpoint(path) {
+      extends API_Endpoint(path) {
 
       def reply(request: HTTP.Request): HTTP.Response = {
         progress.echo_if(verbose, "DOWNLOAD " + description)
@@ -447,13 +458,13 @@
           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)))
+            html_content(render(error_model))
         }
       }
     }
 
     class Post(path: Path, description: String, post: Params.Data => Option[A])
-      extends Endpoint(path, method = "POST") {
+      extends API_Endpoint(path, method = "POST") {
 
       def reply(request: HTTP.Request): HTTP.Response = {
         progress.echo_if(verbose, "POST " + description)
@@ -469,7 +480,8 @@
               progress.echo_if(verbose, "Parsing failed")
               error_model
           }
-        HTTP.Response.html(output_document(render(model)))
+
+        html_content(render(model))
       }
     }