--- a/src/Pure/General/sha1.scala Wed Nov 18 21:34:13 2020 +0100
+++ b/src/Pure/General/sha1.scala Wed Nov 18 21:39:55 2020 +0100
@@ -66,6 +66,8 @@
def digest(bytes: Bytes): Digest = bytes.sha1_digest
def digest(string: String): Digest = digest(Bytes(string))
+ def digest_set(digests: List[Digest]): Digest =
+ digest(cat_lines(digests.map(_.toString).sorted))
val digest_length: Int = digest("").rep.length
}
--- a/src/Pure/Thy/presentation.scala Wed Nov 18 21:34:13 2020 +0100
+++ b/src/Pure/Thy/presentation.scala Wed Nov 18 21:39:55 2020 +0100
@@ -440,7 +440,7 @@
val (doc_dir, root) = prepare_dir1(tmp_dir, doc)
val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
- val sources = SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
+ val sources = SHA1.digest_set(digests).toString
prepare_dir2(tmp_dir, doc)
doc_output.foreach(prepare_dir1(_, doc))
--- a/src/Pure/Tools/build.scala Wed Nov 18 21:34:13 2020 +0100
+++ b/src/Pure/Tools/build.scala Wed Nov 18 21:39:55 2020 +0100
@@ -533,7 +533,7 @@
full_sessions(session_name).meta_digest ::
deps.sources(session_name) :::
deps.imported_sources(session_name)
- SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
+ SHA1.digest_set(digests).toString
}
val deps =