prefer explicit shasum;
clarified signature;

--- a/src/Pure/ML/ml_heap.scala	Mon Feb 06 11:05:35 2023 +0100
+++ b/src/Pure/ML/ml_heap.scala	Mon Feb 06 12:58:45 2023 +0100
@@ -17,7 +17,7 @@
 
   private val sha1_prefix = "SHA1:"
 
-  def read_digest(heap: Path): Option[String] = {
+  def read_digest(heap: Path): Option[SHA1.Digest] = {
     if (heap.is_file) {
       using(FileChannel.open(heap.java_path, StandardOpenOption.READ)) { file =>
         val len = file.size
@@ -37,7 +37,7 @@
           if (i == n) {
             val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
             val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset)
-            if (prefix == sha1_prefix) Some(s) else None
+            if (prefix == sha1_prefix) Some(SHA1.fake_digest(s)) else None
           }
           else None
         }
@@ -47,10 +47,10 @@
     else None
   }
 
-  def write_digest(heap: Path): String =
+  def write_digest(heap: Path): SHA1.Digest =
     read_digest(heap) getOrElse {
-      val s = SHA1.digest(heap).toString
-      File.append(heap, sha1_prefix + s)
-      s
+      val digest = SHA1.digest(heap)
+      File.append(heap, sha1_prefix + digest.toString)
+      digest
     }
 }

--- a/src/Pure/Thy/sessions.scala	Mon Feb 06 11:05:35 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Feb 06 12:58:45 2023 +0100
@@ -1408,8 +1408,11 @@
     def find_heap(name: String): Option[Path] =
       input_dirs.map(_ + heap(name)).find(_.is_file)
 
-    def find_heap_digest(name: String): Option[String] =
-      find_heap(name).flatMap(ML_Heap.read_digest)
+    def find_heap_shasum(name: String): String =
+      (for {
+        path <- find_heap(name)
+        digest <- ML_Heap.read_digest(path)
+      } yield SHA1.shasum(digest, name) + "\n").getOrElse("")
 
     def the_heap(name: String): Path =
       find_heap(name) getOrElse
@@ -1563,8 +1566,8 @@
           stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.compress)
           stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.compress)
           stmt.string(8) = build.sources
-          stmt.string(9) = cat_lines(build.input_heaps)
-          stmt.string(10) = build.output_heap getOrElse ""
+          stmt.string(9) = build.input_heaps
+          stmt.string(10) = build.output_heap
           stmt.int(11) = build.return_code
           stmt.string(12) = build.uuid
           stmt.execute()
@@ -1606,8 +1609,8 @@
             Some(
               Build.Session_Info(
                 res.string(Session_Info.sources),
-                split_lines(res.string(Session_Info.input_heaps)),
-                res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
+                res.string(Session_Info.input_heaps),
+                res.string(Session_Info.output_heap),
                 res.int(Session_Info.return_code),
                 uuid))
           }

--- a/src/Pure/Tools/build.scala	Mon Feb 06 11:05:35 2023 +0100
+++ b/src/Pure/Tools/build.scala	Mon Feb 06 12:58:45 2023 +0100
@@ -19,8 +19,8 @@
 
   sealed case class Session_Info(
     sources: String,
-    input_heaps: List[String],
-    output_heap: Option[String],
+    input_heaps: String,
+    output_heap: String,
     return_code: Int,
     uuid: String
   ) {
@@ -271,7 +271,7 @@
     // scheduler loop
     case class Result(
       current: Boolean,
-      heap_digest: Option[String],
+      output_heap: String,
       process: Option[Process_Result],
       info: Sessions.Info
     ) {
@@ -298,7 +298,7 @@
 
     @tailrec def loop(
       pending: Queue,
-      running: Map[String, (List[String], Build_Job)],
+      running: Map[String, (String, Build_Job)],
       results: Map[String, Result]
     ): Map[String, Result] = {
       def used_node(i: Int): Boolean =
@@ -315,7 +315,7 @@
           case Some((session_name, (input_heaps, job))) =>
             //{{{ finish job
 
-            val (process_result, heap_digest) = job.join
+            val (process_result, output_heap) = job.join
 
             val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
             val process_result_tail = {
@@ -346,7 +346,7 @@
                 build_log =
                   if (process_result.timeout) build_log.error("Timeout") else build_log,
                 build =
-                  Session_Info(build_deps.sources_shasum(session_name), input_heaps, heap_digest,
+                  Session_Info(build_deps.sources_shasum(session_name), input_heaps, output_heap,
                     process_result.rc, UUID.random().toString)))
 
             // messages
@@ -363,7 +363,7 @@
 
             loop(pending - session_name, running - session_name,
               results +
-                (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
+                (session_name -> Result(false, output_heap, Some(process_result_tail), job.info)))
             //}}}
           case None if running.size < (max_jobs max 1) =>
             //{{{ check/start next job
@@ -372,32 +372,32 @@
                 val ancestor_results =
                   build_deps.sessions_structure.build_requirements(List(session_name)).
                     filterNot(_ == session_name).map(results(_))
-                val ancestor_heaps =
+                val input_heaps =
                   if (ancestor_results.isEmpty) {
-                    List(SHA1.digest(Path.explode("$POLYML_EXE")).toString)
+                    SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE"))) + "\n"
                   }
-                  else ancestor_results.flatMap(_.heap_digest)
+                  else ancestor_results.map(_.output_heap).mkString
 
                 val do_store =
                   build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
 
-                val (current, heap_digest) = {
+                val (current, output_heap) = {
                   store.try_open_database(session_name) match {
                     case Some(db) =>
                       using(db)(store.read_build(_, session_name)) match {
                         case Some(build) =>
-                          val heap_digest = store.find_heap_digest(session_name)
+                          val output_heap = store.find_heap_shasum(session_name)
                           val current =
                             !fresh_build &&
                             build.ok &&
                             build.sources == build_deps.sources_shasum(session_name) &&
-                            build.input_heaps == ancestor_heaps &&
-                            build.output_heap == heap_digest &&
-                            !(do_store && heap_digest.isEmpty)
-                          (current, heap_digest)
-                        case None => (false, None)
+                            build.input_heaps == input_heaps &&
+                            build.output_heap == output_heap &&
+                            !(do_store && output_heap.isEmpty)
+                          (current, output_heap)
+                        case None => (false, "")
                       }
-                    case None => (false, None)
+                    case None => (false, "")
                   }
                 }
                 val all_current = current && ancestor_results.forall(_.current)
@@ -405,13 +405,13 @@
                 if (all_current) {
                   loop(pending - session_name, running,
                     results +
-                      (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
+                      (session_name -> Result(true, output_heap, Some(Process_Result(0)), info)))
                 }
                 else if (no_build) {
                   progress.echo_if(verbose, "Skipping " + session_name + " ...")
                   loop(pending - session_name, running,
                     results +
-                      (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
+                      (session_name -> Result(false, output_heap, Some(Process_Result(1)), info)))
                 }
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
                   progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
@@ -424,12 +424,12 @@
                   val job =
                     new Build_Job(progress, build_deps.background(session_name), store, do_store,
                       log, session_setup, numa_node, queue.command_timings(session_name))
-                  loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
+                  loop(pending, running + (session_name -> (input_heaps, job)), results)
                 }
                 else {
                   progress.echo(session_name + " CANCELLED")
                   loop(pending - session_name, running,
-                    results + (session_name -> Result(false, heap_digest, None, info)))
+                    results + (session_name -> Result(false, output_heap, None, info)))
                 }
               case None => sleep(); loop(pending, running, results)
             }

--- a/src/Pure/Tools/build_job.scala	Mon Feb 06 11:05:35 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Mon Feb 06 12:58:45 2023 +0100
@@ -570,7 +570,7 @@
     else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
   }
 
-  def join: (Process_Result, Option[String]) = {
+  def join: (Process_Result, String) = {
     val result1 = future_result.join
 
     val was_timeout =
@@ -591,6 +591,12 @@
       }
       else None
 
-    (result2, heap_digest)
+    val heap_shasum =
+      heap_digest match {
+        case None => ""
+        case Some(digest) => SHA1.shasum(digest, session_name) + "\n"
+      }
+
+    (result2, heap_shasum)
   }
 }