# HG changeset patch
# User wenzelm
# Date 1675677487 -3600
# Node ID d69732bc3dbe17dfa8b0005713a4372322bc536a
# Parent  775baca8cc8aa45a83c512a87ae35fae48f4949f
prefer explicit shasum;

diff -r 775baca8cc8a -r d69732bc3dbe src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Mon Feb 06 10:30:53 2023 +0100
+++ b/src/Pure/General/sha1.scala	Mon Feb 06 10:58:07 2023 +0100
@@ -51,4 +51,7 @@
     digest(cat_lines(digests.map(_.toString).sorted))
 
   val digest_length: Int = digest("").toString.length
+
+  def shasum(digest: Digest, name: String): String = digest.toString + " " + name
+  def shasum_meta_info(digest: Digest): String = shasum(digest, isabelle.setup.Build.META_INFO)
 }
diff -r 775baca8cc8a -r d69732bc3dbe src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Feb 06 10:30:53 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Feb 06 10:58:07 2023 +0100
@@ -142,6 +142,8 @@
       ", loaded_theories = " + loaded_theories.size +
       ", used_theories = " + used_theories.length
 
+    def all_sources: List[(Path, SHA1.Digest)] = imported_sources ::: session_sources
+
     def all_document_theories: List[Document.Node.Name] =
       proper_session_theories ::: document_theories
 
@@ -273,11 +275,14 @@
     def apply(name: String): Base = session_bases(name)
     def get(name: String): Option[Base] = session_bases.get(name)
 
-    def imported_sources(name: String): List[SHA1.Digest] =
-      session_bases(name).imported_sources.map(_._2)
-
-    def session_sources(name: String): List[SHA1.Digest] =
-      session_bases(name).session_sources.map(_._2)
+    def sources_shasum(name: String): String = {
+      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))
+      Library.terminate_lines(meta_info :: sources)
+    }
 
     def errors: List[String] =
       (for {
diff -r 775baca8cc8a -r d69732bc3dbe src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Feb 06 10:30:53 2023 +0100
+++ b/src/Pure/Tools/build.scala	Mon Feb 06 10:58:07 2023 +0100
@@ -209,14 +209,6 @@
         augment_options = augment_options)
     val full_sessions_selection = full_sessions.imports_selection(selection)
 
-    def sources_stamp(deps: Sessions.Deps, session_name: String): String = {
-      val digests =
-        full_sessions(session_name).meta_digest ::
-        deps.session_sources(session_name) :::
-        deps.imported_sources(session_name)
-      SHA1.digest_set(digests).toString
-    }
-
     val build_deps = {
       val deps0 =
         Sessions.deps(full_sessions.selection(selection),
@@ -230,7 +222,7 @@
               case Some(db) =>
                 using(db)(store.read_build(_, name)) match {
                   case Some(build)
-                  if build.ok && build.sources == sources_stamp(deps0, name) => None
+                  if build.ok && build.sources == deps0.sources_shasum(name) => None
                   case _ => Some(name)
                 }
               case None => Some(name)
@@ -354,7 +346,7 @@
                 build_log =
                   if (process_result.timeout) build_log.error("Timeout") else build_log,
                 build =
-                  Session_Info(sources_stamp(build_deps, session_name), input_heaps, heap_digest,
+                  Session_Info(build_deps.sources_shasum(session_name), input_heaps, heap_digest,
                     process_result.rc, UUID.random().toString)))
 
             // messages
@@ -398,7 +390,7 @@
                           val current =
                             !fresh_build &&
                             build.ok &&
-                            build.sources == sources_stamp(build_deps, session_name) &&
+                            build.sources == build_deps.sources_shasum(session_name) &&
                             build.input_heaps == ancestor_heaps &&
                             build.output_heap == heap_digest &&
                             !(do_store && heap_digest.isEmpty)