proper Shasum.digest, to emulate old form from build_history database;
clarified signature: more explicit types;

--- a/src/Pure/Admin/build_history.scala	Mon Feb 06 12:58:45 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Mon Feb 06 14:54:15 2023 +0100
@@ -295,8 +295,8 @@
 
               val session_sources =
                 store.read_build(db, session_name).map(_.sources) match {
-                  case Some(sources) if sources.length == SHA1.digest_length =>
-                    List("Sources " + session_name + " " + sources)
+                  case Some(sources) if !sources.is_empty =>
+                    List("Sources " + session_name + " " + sources.digest.toString)
                   case _ => Nil
                 }
 

--- a/src/Pure/General/sha1.scala	Mon Feb 06 12:58:45 2023 +0100
+++ b/src/Pure/General/sha1.scala	Mon Feb 06 14:54:15 2023 +0100
@@ -14,6 +14,8 @@
 
 
 object SHA1 {
+  /* digest */
+
   final class Digest private[SHA1](rep: String) {
     override def toString: String = rep
     override def hashCode: Int = rep.hashCode
@@ -52,6 +54,33 @@
 
   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)
+
+  /* shasum */
+
+  final class Shasum private[SHA1](private[SHA1] val rep: List[String]) {
+    override def equals(other: Any): Boolean =
+      other match {
+        case that: Shasum => rep.equals(that.rep)
+        case _ => false
+      }
+    override def hashCode: Int = rep.hashCode
+    override def toString: String = Library.terminate_lines(rep)
+
+    def is_empty: Boolean = rep.isEmpty
+
+    def digest: Digest = {
+      rep match {
+        case List(s)
+        if s.length == digest_length && s.forall(Symbol.is_ascii_hex) => fake_digest(s)
+        case _ => SHA1.digest(toString)
+      }
+    }
+  }
+
+  val no_shasum: Shasum = new Shasum(Nil)
+  def flat_shasum(list: List[Shasum]): Shasum = new Shasum(list.flatMap(_.rep))
+  def fake_shasum(text: String): Shasum = new Shasum(Library.trim_split_lines(text))
+
+  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)
 }

--- a/src/Pure/Thy/sessions.scala	Mon Feb 06 12:58:45 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Feb 06 14:54:15 2023 +0100
@@ -275,13 +275,14 @@
     def apply(name: String): Base = session_bases(name)
     def get(name: String): Option[Base] = session_bases.get(name)
 
-    def sources_shasum(name: String): String = {
+    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))
-      Library.terminate_lines(meta_info :: sources)
+
+      SHA1.flat_shasum(meta_info :: sources)
     }
 
     def errors: List[String] =
@@ -1408,11 +1409,11 @@
     def find_heap(name: String): Option[Path] =
       input_dirs.map(_ + heap(name)).find(_.is_file)
 
-    def find_heap_shasum(name: String): String =
+    def find_heap_shasum(name: String): SHA1.Shasum =
       (for {
         path <- find_heap(name)
         digest <- ML_Heap.read_digest(path)
-      } yield SHA1.shasum(digest, name) + "\n").getOrElse("")
+      } yield SHA1.shasum(digest, name)).getOrElse(SHA1.no_shasum)
 
     def the_heap(name: String): Path =
       find_heap(name) getOrElse
@@ -1565,9 +1566,9 @@
           stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.compress)
           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) = build.input_heaps
-          stmt.string(10) = build.output_heap
+          stmt.string(8) = build.sources.toString
+          stmt.string(9) = build.input_heaps.toString
+          stmt.string(10) = build.output_heap.toString
           stmt.int(11) = build.return_code
           stmt.string(12) = build.uuid
           stmt.execute()
@@ -1608,9 +1609,9 @@
               catch { case _: SQLException => "" }
             Some(
               Build.Session_Info(
-                res.string(Session_Info.sources),
-                res.string(Session_Info.input_heaps),
-                res.string(Session_Info.output_heap),
+                SHA1.fake_shasum(res.string(Session_Info.sources)),
+                SHA1.fake_shasum(res.string(Session_Info.input_heaps)),
+                SHA1.fake_shasum(res.string(Session_Info.output_heap)),
                 res.int(Session_Info.return_code),
                 uuid))
           }

--- a/src/Pure/Tools/build.scala	Mon Feb 06 12:58:45 2023 +0100
+++ b/src/Pure/Tools/build.scala	Mon Feb 06 14:54:15 2023 +0100
@@ -18,9 +18,9 @@
   /* persistent build info */
 
   sealed case class Session_Info(
-    sources: String,
-    input_heaps: String,
-    output_heap: String,
+    sources: SHA1.Shasum,
+    input_heaps: SHA1.Shasum,
+    output_heap: SHA1.Shasum,
     return_code: Int,
     uuid: String
   ) {
@@ -271,7 +271,7 @@
     // scheduler loop
     case class Result(
       current: Boolean,
-      output_heap: String,
+      output_heap: SHA1.Shasum,
       process: Option[Process_Result],
       info: Sessions.Info
     ) {
@@ -298,7 +298,7 @@
 
     @tailrec def loop(
       pending: Queue,
-      running: Map[String, (String, Build_Job)],
+      running: Map[String, (SHA1.Shasum, Build_Job)],
       results: Map[String, Result]
     ): Map[String, Result] = {
       def used_node(i: Int): Boolean =
@@ -374,9 +374,9 @@
                     filterNot(_ == session_name).map(results(_))
                 val input_heaps =
                   if (ancestor_results.isEmpty) {
-                    SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE"))) + "\n"
+                    SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
                   }
-                  else ancestor_results.map(_.output_heap).mkString
+                  else SHA1.flat_shasum(ancestor_results.map(_.output_heap))
 
                 val do_store =
                   build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
@@ -393,11 +393,11 @@
                             build.sources == build_deps.sources_shasum(session_name) &&
                             build.input_heaps == input_heaps &&
                             build.output_heap == output_heap &&
-                            !(do_store && output_heap.isEmpty)
+                            !(do_store && output_heap.is_empty)
                           (current, output_heap)
-                        case None => (false, "")
+                        case None => (false, SHA1.no_shasum)
                       }
-                    case None => (false, "")
+                    case None => (false, SHA1.no_shasum)
                   }
                 }
                 val all_current = current && ancestor_results.forall(_.current)

--- a/src/Pure/Tools/build_job.scala	Mon Feb 06 12:58:45 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Mon Feb 06 14:54:15 2023 +0100
@@ -570,7 +570,7 @@
     else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
   }
 
-  def join: (Process_Result, String) = {
+  def join: (Process_Result, SHA1.Shasum) = {
     val result1 = future_result.join
 
     val was_timeout =
@@ -585,17 +585,11 @@
       else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt"))
       else result1
 
-    val heap_digest =
+    val heap_shasum =
       if (result2.ok && do_store && store.output_heap(session_name).is_file) {
-        Some(ML_Heap.write_digest(store.output_heap(session_name)))
+        SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name)
       }
-      else None
-
-    val heap_shasum =
-      heap_digest match {
-        case None => ""
-        case Some(digest) => SHA1.shasum(digest, session_name) + "\n"
-      }
+      else SHA1.no_shasum
 
     (result2, heap_shasum)
   }