more efficient equals: avoid somewhat slow sha1_digest (see also 29b761e290c5, 306f273c91ec);

--- a/src/Pure/General/bytes.scala	Sat Jun 15 21:59:31 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sat Jun 15 22:43:01 2024 +0200
@@ -384,11 +384,17 @@
       case other: Bytes =>
         if (this.eq(other)) true
         else if (size != other.size) false
-        else if (chunks.isEmpty && size <= 10 * SHA1.digest_length) {
-          Arrays.equals(chunk0, offset.toInt, (offset + size).toInt,
-            other.chunk0, other.offset.toInt, (other.offset + other.size).toInt)
+        else {
+          if (chunks.isEmpty && other.chunks.isEmpty) {
+            Arrays.equals(chunk0, offset.toInt, (offset + size).toInt,
+              other.chunk0, other.offset.toInt, (other.offset + other.size).toInt)
+          }
+          else if (!is_sliced && !other.is_sliced) {
+            (subarray_iterator zip other.subarray_iterator)
+              .forall((a, b) => Arrays.equals(a.array, b.array))
+          }
+          else sha1_digest == other.sha1_digest
         }
-        else sha1_digest == other.sha1_digest
       case _ => false
     }
   }

--- a/src/Pure/General/file.scala	Sat Jun 15 21:59:31 2024 +0200
+++ b/src/Pure/General/file.scala	Sat Jun 15 22:43:01 2024 +0200
@@ -355,7 +355,7 @@
   def eq_content(file1: JFile, file2: JFile): Boolean =
     if (eq(file1, file2)) true
     else if (file1.length != file2.length) false
-    else SHA1.digest(file1) == SHA1.digest(file2)
+    else Bytes.read(file1) == Bytes.read(file2)
 
   def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file)