# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1717610794 -7200
# Node ID df8fa0393127593e4be6e7b342ece0aa003f8f44
# Parent  1844c169e36013a2dc78ee2211c6afdd2d2d501d
web app: add automatic resize;

diff -r 1844c169e360 -r df8fa0393127 src/Pure/System/web_app.scala
--- a/src/Pure/System/web_app.scala	Wed Jun 05 17:41:16 2024 +0200
+++ b/src/Pure/System/web_app.scala	Wed Jun 05 20:06:34 2024 +0200
@@ -401,9 +401,7 @@
       extends Endpoint(paths.api_path(path, external = false), method) {
 
       def html_content(content: XML.Body, auto_reload: Boolean = false): HTTP.Response = {
-        val head1 =
-          if (!auto_reload) head
-          else HTML.script("""
+        val auto_reload_script = HTML.script("""
 var state = null
 function heartbeat() {
   fetch(window.location, { method: "HEAD" }).then((http_res) => {
@@ -415,13 +413,21 @@
     setTimeout(heartbeat, 1000)
   })
 }
-heartbeat()""") :: head
+heartbeat()""")
 
-        val on_load = "parent.postMessage(document.documentElement.scrollHeight, '*')"
+        val resize_script = HTML.script("""
+function post_height() {
+  const scroll_bar_height = window.innerHeight - document.documentElement.clientHeight
+  parent.postMessage(document.documentElement.scrollHeight + scroll_bar_height, '*')
+}
+window.addEventListener("resize", (event) => { post_height() })
+""")
+
+        val head1 = (if (auto_reload) List(auto_reload_script) else Nil) ::: resize_script :: head
 
         html(
           XML.elem("head", HTML.head_meta :: head1),
-          XML.Elem(Markup("body", List("onLoad" -> on_load)), content))
+          XML.Elem(Markup("body", List("onLoad" -> "post_height()")), content))
       }
     }