# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1717435282 -7200
# Node ID b2889dd54a2af59c1bf414722878ae37b4d8fd06
# Parent  5cb9fd414e92c839454b26fcc1af49edb6ce5680
use Content-Digest header in HEAD requests instead of length (to track non-monotone changes);

diff -r 5cb9fd414e92 -r b2889dd54a2a src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Mon Jun 03 20:56:41 2024 +0100
+++ b/src/Pure/General/http.scala	Mon Jun 03 19:21:22 2024 +0200
@@ -10,6 +10,7 @@
 import java.io.{File => JFile}
 import java.nio.file.Files
 import java.net.{InetSocketAddress, URI, HttpURLConnection}
+import java.util.HexFormat
 import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
 
 
@@ -222,7 +223,10 @@
 
     def write(http: HttpExchange, code: Int, is_head: Boolean = false): Unit = {
       http.getResponseHeaders.set("Content-Type", content_type)
-      http.getResponseHeaders.set("Content-Length", output.length.toString)
+      if (is_head) {
+        val encoded_digest = Base64.encode(HexFormat.of().parseHex(SHA1.digest(output).toString))
+        http.getResponseHeaders.set("Content-Digest", "sha=:" + encoded_digest + ":")
+      }
       http.sendResponseHeaders(code, if (is_head) -1 else output.length.toLong)
       if (!is_head) using(http.getResponseBody)(output.write_stream)
     }
diff -r 5cb9fd414e92 -r b2889dd54a2a src/Pure/System/web_app.scala
--- a/src/Pure/System/web_app.scala	Mon Jun 03 20:56:41 2024 +0100
+++ b/src/Pure/System/web_app.scala	Mon Jun 03 19:21:22 2024 +0200
@@ -407,7 +407,7 @@
 var state = null;
 function heartbeat() {
   fetch(window.location, { method: "HEAD" }).then((http_res) => {
-    const new_state = http_res.headers.get("Content-Length")
+    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