--- 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),