# HG changeset patch
# User wenzelm
# Date 1739461011 -3600
# Node ID 7d579158d186a99f05ac87b1257752eaa1e83d12
# Parent  0c8052a5bbf6be85cf7ae5a3da996b0013d681ee
clarified signature: more explicit operations;

diff -r 0c8052a5bbf6 -r 7d579158d186 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Feb 13 16:29:25 2025 +0100
+++ b/src/Pure/General/http.scala	Thu Feb 13 16:36:51 2025 +0100
@@ -11,7 +11,6 @@
 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}
 
 
@@ -240,8 +239,8 @@
     def write(http: HttpExchange, code: Int, is_head: Boolean = false): Unit = {
       http.getResponseHeaders.set("Content-Type", content_type)
       if (is_head) {
-        val encoded_digest = Base64.encode(HexFormat.of().parseHex(SHA1.digest(output).toString))
-        http.getResponseHeaders.set("Content-Digest", "sha=:" + encoded_digest + ":")
+        val digest_base64 = SHA1.digest(output).base64
+        http.getResponseHeaders.set("Content-Digest", "sha=:" + digest_base64 + ":")
       }
       http.sendResponseHeaders(code, if (is_head) -1 else output.size)
       if (!is_head) using(http.getResponseBody)(output.write_stream)
diff -r 0c8052a5bbf6 -r 7d579158d186 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Thu Feb 13 16:29:25 2025 +0100
+++ b/src/Pure/General/sha1.scala	Thu Feb 13 16:36:51 2025 +0100
@@ -9,6 +9,7 @@
 
 import java.io.{File => JFile, FileInputStream}
 import java.security.MessageDigest
+import java.util.HexFormat
 
 import isabelle.setup.{Build => Setup_Build}
 
@@ -24,6 +25,7 @@
         case other: Digest => rep == other.toString
         case _ => false
       }
+    def base64: String = Base64.encode(HexFormat.of().parseHex(rep))
   }
 
   def fake_digest(rep: String): Digest = new Digest(rep)