# HG changeset patch
# User wenzelm
# Date 1393585480 -3600
# Node ID f7ceebe2f1b5589f713c419801046038cfd57890
# Parent  28b59620f0d096064a181fe7f79ddc05b2a5756b
prefer abstract datatype -- in accordance to ML version;

diff -r 28b59620f0d0 -r f7ceebe2f1b5 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Fri Feb 28 11:58:26 2014 +0100
+++ b/src/Pure/General/sha1.scala	Fri Feb 28 12:04:40 2014 +0100
@@ -14,8 +14,14 @@
 
 object SHA1
 {
-  sealed case class Digest(rep: String)
+  final class Digest private[SHA1](val rep: String)
   {
+    override def hashCode: Int = rep.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Digest => rep == other.rep
+        case _ => false
+      }
     override def toString: String = rep
   }
 
@@ -27,7 +33,7 @@
       if (i < 16) result += '0'
       result ++= Integer.toHexString(i)
     }
-    Digest(result.toString)
+    new Digest(result.toString)
   }
 
   def digest(file: JFile): Digest =