# 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 */