--- 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)))
}
--- 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 */
--- 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] =