38473
|
1 |
/* Title: Pure/General/sha1.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
41954
|
4 |
Digest strings according to SHA-1 (see RFC 3174).
|
38473
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
|
10 |
import java.security.MessageDigest
|
|
11 |
|
|
12 |
|
|
13 |
object SHA1
|
|
14 |
{
|
43714
|
15 |
sealed case class Digest(rep: String)
|
41954
|
16 |
{
|
|
17 |
override def toString: String = rep
|
|
18 |
}
|
|
19 |
|
|
20 |
def digest_bytes(bytes: Array[Byte]): Digest =
|
38473
|
21 |
{
|
|
22 |
val result = new StringBuilder
|
|
23 |
for (b <- MessageDigest.getInstance("SHA").digest(bytes)) {
|
|
24 |
val i = b.asInstanceOf[Int] & 0xFF
|
|
25 |
if (i < 16) result += '0'
|
|
26 |
result ++= Integer.toHexString(i)
|
|
27 |
}
|
41954
|
28 |
Digest(result.toString)
|
38473
|
29 |
}
|
|
30 |
|
41954
|
31 |
def digest(s: String): Digest = digest_bytes(Standard_System.string_bytes(s))
|
38473
|
32 |
}
|
|
33 |
|