# HG changeset patch
# User wenzelm
# Date 1675695857 -3600
# Node ID df8d71edbc79f2e6577acbe87faae36efa6b1a06
# Parent  05a4ce3f6b0c1bbe3afabbee84e19163af608ce0
clarified signature, using right-associative operation;

diff -r 05a4ce3f6b0c -r df8d71edbc79 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Mon Feb 06 15:53:58 2023 +0100
+++ b/src/Pure/General/sha1.scala	Mon Feb 06 16:04:17 2023 +0100
@@ -67,6 +67,8 @@
 
     def is_empty: Boolean = rep.isEmpty
 
+    def :::(other: Shasum): Shasum = new Shasum(other.rep ::: rep)
+
     def digest: Digest = {
       rep match {
         case List(s)
diff -r 05a4ce3f6b0c -r df8d71edbc79 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Mon Feb 06 15:53:58 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Mon Feb 06 16:04:17 2023 +0100
@@ -313,7 +313,7 @@
           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(List(meta_info, manifest))
+      val sources = meta_info ::: manifest
 
 
       /* derived material: without SHA1 digest */
diff -r 05a4ce3f6b0c -r df8d71edbc79 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Feb 06 15:53:58 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Feb 06 16:04:17 2023 +0100
@@ -281,7 +281,7 @@
         SHA1.shasum_sorted(
           for ((path, digest) <- apply(name).all_sources)
             yield digest -> File.symbolic_path(path))
-      SHA1.flat_shasum(List(meta_info, sources))
+      meta_info ::: sources
     }
 
     def errors: List[String] =