author | wenzelm |
Mon, 28 Nov 2011 22:18:19 +0100 | |
changeset 45667 | 546d78f0d81f |
parent 43714 | 3749d1e6dde9 |
child 45673 | cd41e3903fbf |
permissions | -rw-r--r-- |
38473 | 1 |
/* Title: Pure/General/sha1.scala |
45667
546d78f0d81f
explicit indication of modules for independent Scala library;
wenzelm
parents:
43714
diff
changeset
|
2 |
Module: Library |
38473 | 3 |
Author: Makarius |
4 |
||
41954 | 5 |
Digest strings according to SHA-1 (see RFC 3174). |
38473 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
11 |
import java.security.MessageDigest |
|
12 |
||
13 |
||
14 |
object SHA1 |
|
15 |
{ |
|
43714 | 16 |
sealed case class Digest(rep: String) |
41954 | 17 |
{ |
18 |
override def toString: String = rep |
|
19 |
} |
|
20 |
||
21 |
def digest_bytes(bytes: Array[Byte]): Digest = |
|
38473 | 22 |
{ |
23 |
val result = new StringBuilder |
|
24 |
for (b <- MessageDigest.getInstance("SHA").digest(bytes)) { |
|
25 |
val i = b.asInstanceOf[Int] & 0xFF |
|
26 |
if (i < 16) result += '0' |
|
27 |
result ++= Integer.toHexString(i) |
|
28 |
} |
|
41954 | 29 |
Digest(result.toString) |
38473 | 30 |
} |
31 |
||
41954 | 32 |
def digest(s: String): Digest = digest_bytes(Standard_System.string_bytes(s)) |
38473 | 33 |
} |
34 |