tuned;
authorFabian Huch <huch@in.tum.de>
Mon, 03 Jun 2024 19:37:42 +0200
changeset 80244 885fc1e837ed
parent 80243 b2889dd54a2a
child 80245 b6551e0c70c4
tuned;
src/Pure/System/web_app.scala
--- a/src/Pure/System/web_app.scala	Mon Jun 03 19:21:22 2024 +0200
+++ b/src/Pure/System/web_app.scala	Mon Jun 03 19:37:42 2024 +0200
@@ -404,19 +404,18 @@
         val head1 =
           if (!auto_reload) head
           else HTML.script("""
-var state = null;
+var state = null
 function heartbeat() {
   fetch(window.location, { method: "HEAD" }).then((http_res) => {
-    const new_state = http_res.headers.get("Content-Digest")
-    if (state === null) state = new_state
-    if (http_res.status === 200 && state !== new_state) {
-      state = new_state
-      window.location.reload()
+    if (http_res.status === 200) {
+      const new_state = http_res.headers.get("Content-Digest")
+      if (state === null) state = new_state
+      else if (state !== new_state) window.location.reload()
     }
-    setTimeout(heartbeat, 1000);
+    setTimeout(heartbeat, 1000)
   })
 }
-setTimeout(heartbeat, 1000);""") :: head
+heartbeat()""") :: head
 
         html(
           XML.elem("head", HTML.head_meta :: head1),