tuned signature;

--- a/src/Pure/General/sha1.scala	Wed Mar 23 12:02:56 2022 +0100
+++ b/src/Pure/General/sha1.scala	Wed Mar 23 12:15:25 2022 +0100
@@ -15,15 +15,15 @@
 
 object SHA1
 {
-  final class Digest private[SHA1](val rep: String)
+  final class Digest private[SHA1](rep: String)
   {
+    override def toString: String = rep
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
       that match {
-        case other: Digest => rep == other.rep
+        case other: Digest => rep == other.toString
         case _ => false
       }
-    override def toString: String = rep
   }
 
   def fake_digest(rep: String): Digest = new Digest(rep)
@@ -52,5 +52,5 @@
   def digest_set(digests: List[Digest]): Digest =
     digest(cat_lines(digests.map(_.toString).sorted))
 
-  val digest_length: Int = digest("").rep.length
+  val digest_length: Int = digest("").toString.length
 }

--- a/src/Pure/System/components.scala	Wed Mar 23 12:02:56 2022 +0100
+++ b/src/Pure/System/components.scala	Wed Mar 23 12:15:25 2022 +0100
@@ -303,8 +303,7 @@
         yield {
           val file_name = archive.file_name
           progress.echo("Digesting local " + file_name)
-          val sha1 = SHA1.digest(archive).rep
-          SHA1_Digest(sha1, file_name)
+          SHA1_Digest(SHA1.digest(archive).toString, file_name)
         }
       val new_names = new_entries.map(_.file_name).toSet
 

--- a/src/Pure/Thy/sessions.scala	Wed Mar 23 12:02:56 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Mar 23 12:15:25 2022 +0100
@@ -1172,7 +1172,7 @@
   def write_heap_digest(heap: Path): String =
     read_heap_digest(heap) match {
       case None =>
-        val s = SHA1.digest(heap).rep
+        val s = SHA1.digest(heap).toString
         File.append(heap, sha1_prefix + s)
         s
       case Some(s) => s