web app: proper document height;
authorFabian Huch <huch@in.tum.de>
Tue, 04 Jun 2024 18:24:38 +0200
changeset 80249 58881e1e4a75
parent 80248 95f169ac0207
child 80250 8ae6f4e8cc2a
web app: proper document height;
src/Pure/System/web_app.scala
--- a/src/Pure/System/web_app.scala	Tue Jun 04 18:08:47 2024 +0200
+++ b/src/Pure/System/web_app.scala	Tue Jun 04 18:24:38 2024 +0200
@@ -372,7 +372,7 @@
 (function() {
   window.addEventListener('message', (event) => {
     if (Number.isInteger(event.data)) {
-      this.style.height=event.data + 32 + 'px'
+      this.style.height=event.data + 'px'
     }
   })
 }).call(this)"""
@@ -417,11 +417,11 @@
 }
 heartbeat()""") :: head
 
+        val on_load = "parent.postMessage(document.documentElement.scrollHeight, '*')"
+
         html(
           XML.elem("head", HTML.head_meta :: head1),
-          XML.Elem(
-            Markup("body", List("onLoad" -> "parent.postMessage(document.body.scrollHeight, '*')")),
-            content))
+          XML.Elem(Markup("body", List("onLoad" -> on_load)), content))
       }
     }