# HG changeset patch
# User wenzelm
# Date 1675692667 -3600
# Node ID 3070001c9d1f809c80bdc16e05ebcb8943b39e47
# Parent  a3f67a4459e1b00b2149c1d764dac8c848f3b2b7
tuned signature;

diff -r a3f67a4459e1 -r 3070001c9d1f src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Mon Feb 06 15:04:21 2023 +0100
+++ b/src/Pure/General/sha1.scala	Mon Feb 06 15:11:07 2023 +0100
@@ -24,7 +24,6 @@
         case other: Digest => rep == other.toString
         case _ => false
       }
-    def shasum(name: String): String = rep + " " + name
   }
 
   def fake_digest(rep: String): Digest = new Digest(rep)
diff -r a3f67a4459e1 -r 3070001c9d1f src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Mon Feb 06 15:04:21 2023 +0100
+++ b/src/Pure/System/components.scala	Mon Feb 06 15:11:07 2023 +0100
@@ -217,19 +217,19 @@
 
   val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1")
 
-  sealed case class SHA1_Digest(digest: SHA1.Digest, name: String) {
-    override def toString: String = digest.shasum(name)
+  sealed case class SHA1_Entry(digest: SHA1.Digest, name: String) {
+    override def toString: String = SHA1.shasum(digest, name).toString
   }
 
-  def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] =
+  def read_components_sha1(lines: List[String] = Nil): List[SHA1_Entry] =
     (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line =>
       Word.explode(line) match {
         case Nil => None
-        case List(sha1, name) => Some(SHA1_Digest(SHA1.fake_digest(sha1), name))
+        case List(sha1, name) => Some(SHA1_Entry(SHA1.fake_digest(sha1), name))
         case _ => error("Bad components.sha1 entry: " + quote(line))
       })
 
-  def write_components_sha1(entries: List[SHA1_Digest]): Unit =
+  def write_components_sha1(entries: List[SHA1_Entry]): Unit =
     File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n"))
 
 
@@ -384,7 +384,7 @@
         yield {
           val name = archive.file_name
           progress.echo("Digesting local " + name)
-          SHA1_Digest(SHA1.digest(archive), name)
+          SHA1_Entry(SHA1.digest(archive), name)
         }
       val new_names = new_entries.map(_.name).toSet