# HG changeset patch
# User wenzelm
# Date 1718221213 -7200
# Node ID bb4e95d19ecb09c3a2dc832cd619ba76b808754c
# Parent  45b434464cd83fc1921b55dc8f5fcc65b50e4769
minor performance tuning;

diff -r 45b434464cd8 -r bb4e95d19ecb src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Wed Jun 12 16:58:55 2024 +0200
+++ b/src/Pure/General/bytes.scala	Wed Jun 12 21:40:13 2024 +0200
@@ -158,7 +158,8 @@
   /* content */
 
   lazy val sha1_digest: SHA1.Digest =
-    SHA1.make_digest { sha => sha.update(bytes, offset, length) }
+    if (is_empty) SHA1.digest_empty
+    else SHA1.make_digest { sha => sha.update(bytes, offset, length) }
 
   def is_empty: Boolean = length == 0
 
diff -r 45b434464cd8 -r bb4e95d19ecb src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Wed Jun 12 16:58:55 2024 +0200
+++ b/src/Pure/General/sha1.scala	Wed Jun 12 21:40:13 2024 +0200
@@ -33,6 +33,9 @@
     new Digest(Setup_Build.make_digest(digest_body))
   }
 
+  val digest_empty: Digest = make_digest(_ => ())
+  def digest_length: Int = digest_empty.toString.length
+
   def digest(file: JFile): Digest =
     make_digest(sha => using(new FileInputStream(file)) { stream =>
       val buf = new Array[Byte](65536)
@@ -49,8 +52,6 @@
   def digest(bytes: Bytes): Digest = bytes.sha1_digest
   def digest(string: String): Digest = digest(Bytes(string))
 
-  val digest_length: Int = digest("").toString.length
-
 
   /* shasum */