# HG changeset patch
# User wenzelm
# Date 1675694787 -3600
# Node ID a917f580a10705e13523b7fb9619e8cca4af9318
# Parent  1ffee8893b12ed2e3513c50a6207f17e3707fa8c
clarified signature;

diff -r 1ffee8893b12 -r a917f580a107 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Mon Feb 06 15:35:18 2023 +0100
+++ b/src/Pure/General/sha1.scala	Mon Feb 06 15:46:27 2023 +0100
@@ -82,4 +82,6 @@
 
   def shasum(digest: Digest, name: String): Shasum = new Shasum(List(digest.toString + " " + name))
   def shasum_meta_info(digest: Digest): Shasum = shasum(digest, isabelle.setup.Build.META_INFO)
+  def shasum_sorted(args: List[(Digest, String)]): Shasum =
+    flat_shasum(args.sortBy(_._2).map(arg => shasum(arg._1, arg._2)))
 }
diff -r 1ffee8893b12 -r a917f580a107 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon Feb 06 15:35:18 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Mon Feb 06 15:46:27 2023 +0100
@@ -309,11 +309,11 @@
           SHA1.digest(List(doc.print, document_logo.toString, document_build).toString))
 
       val manifest =
-        (for (file <- File.find_files(doc_dir.file, follow_links = true))
-          yield File.path(doc_dir.java_path.relativize(file.toPath)).implode -> SHA1.digest(file))
-        .sortBy(_._1).map(p => SHA1.shasum(p._2, p._1))
+        SHA1.shasum_sorted(
+          for (file <- File.find_files(doc_dir.file, follow_links = true))
+            yield SHA1.digest(file) -> File.path(doc_dir.java_path.relativize(file.toPath)).implode)
 
-      val sources = SHA1.flat_shasum(meta_info :: manifest)
+      val sources = SHA1.flat_shasum(List(meta_info, manifest))
 
 
       /* derived material: without SHA1 digest */
diff -r 1ffee8893b12 -r a917f580a107 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Feb 06 15:35:18 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Feb 06 15:46:27 2023 +0100
@@ -278,11 +278,10 @@
     def sources_shasum(name: String): SHA1.Shasum = {
       val meta_info = SHA1.shasum_meta_info(sessions_structure(name).meta_digest)
       val sources =
-        (for ((path, digest) <- apply(name).all_sources)
-          yield (File.symbolic_path(path), digest))
-        .sortBy(_._1).map(p => SHA1.shasum(p._2, p._1))
-
-      SHA1.flat_shasum(meta_info :: sources)
+        SHA1.shasum_sorted(
+          for ((path, digest) <- apply(name).all_sources)
+            yield digest -> File.symbolic_path(path))
+      SHA1.flat_shasum(List(meta_info, sources))
     }
 
     def errors: List[String] =