add auto-reload for more interactive web apps;
authorFabian Huch <huch@in.tum.de>
Wed, 29 May 2024 15:09:48 +0200
changeset 80205 fc2d791d28bd
parent 80204 81f2fbf3975d
child 80206 3cf3ad092e3e
add auto-reload for more interactive web apps;
src/Pure/System/web_app.scala
--- a/src/Pure/System/web_app.scala	Wed May 29 14:55:36 2024 +0200
+++ b/src/Pure/System/web_app.scala	Wed May 29 15:09:48 2024 +0200
@@ -402,12 +402,30 @@
     sealed abstract class API_Endpoint(path: Path, method: String = "GET")
       extends Endpoint(paths.api_path(path, external = false), method) {
 
-      def html_content(content: XML.Body): HTTP.Response =
+      def html_content(content: XML.Body, auto_reload: Boolean = false): HTTP.Response = {
+        val head1 =
+          if (!auto_reload) head
+          else HTML.script("""
+var state = null;
+function heartbeat() {
+  fetch(window.location, { method: "HEAD" }).then((http_res) => {
+    const new_state = http_res.headers.get("Content-Length")
+    if (state === null) state = new_state
+    if (http_res.status === 200 && state !== new_state) {
+      state = new_state
+      window.location.reload()
+    }
+    setTimeout(heartbeat, 1000);
+  })
+}
+setTimeout(heartbeat, 1000);""") :: head
+
         html(
-          XML.elem("head", HTML.head_meta :: head),
+          XML.elem("head", HTML.head_meta :: head1),
           XML.Elem(
             Markup("body", List("onLoad" -> "parent.postMessage(document.body.scrollHeight, '*')")),
             content))
+      }
     }
 
     private def query_params(request: HTTP.Request): Properties.T = {
@@ -441,7 +459,7 @@
               error_model
           }
 
-        html_content(render(model))
+        html_content(render(model), auto_reload = true)
       }
     }