| author | wenzelm |
| Sat, 31 Mar 2012 19:38:41 +0200 | |
| changeset 47240 | 72ab1fbf2f41 |
| parent 45673 | cd41e3903fbf |
| child 48343 | 3060e6343953 |
| permissions | -rw-r--r-- |
| 38473 | 1 |
/* Title: Pure/General/sha1.scala |
|
45673
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents:
45667
diff
changeset
|
2 |
Module: PIDE |
| 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 |