| author | nipkow | 
| Thu, 18 Apr 2013 20:18:50 +0200 | |
| changeset 51716 | 89f0d01371a8 | 
| parent 50203 | 00d8ad713e32 | 
| child 54440 | 2c4940d2edf7 | 
| 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: 
45667diff
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 | ||
| 48409 | 11 | import java.io.{File => JFile, FileInputStream}
 | 
| 38473 | 12 | import java.security.MessageDigest | 
| 13 | ||
| 14 | ||
| 15 | object SHA1 | |
| 16 | {
 | |
| 43714 | 17 | sealed case class Digest(rep: String) | 
| 41954 | 18 |   {
 | 
| 19 | override def toString: String = rep | |
| 20 | } | |
| 21 | ||
| 48343 | 22 | private def make_result(digest: MessageDigest): Digest = | 
| 38473 | 23 |   {
 | 
| 24 | val result = new StringBuilder | |
| 48343 | 25 |     for (b <- digest.digest()) {
 | 
| 38473 | 26 | val i = b.asInstanceOf[Int] & 0xFF | 
| 27 | if (i < 16) result += '0' | |
| 28 | result ++= Integer.toHexString(i) | |
| 29 | } | |
| 41954 | 30 | Digest(result.toString) | 
| 38473 | 31 | } | 
| 32 | ||
| 48409 | 33 | def digest(file: JFile): Digest = | 
| 48343 | 34 |   {
 | 
| 35 | val stream = new FileInputStream(file) | |
| 36 |     val digest = MessageDigest.getInstance("SHA")
 | |
| 37 | ||
| 38 | val buf = new Array[Byte](65536) | |
| 39 | var m = 0 | |
| 40 |     try {
 | |
| 41 |       do {
 | |
| 42 | m = stream.read(buf, 0, buf.length) | |
| 43 | if (m != -1) digest.update(buf, 0, m) | |
| 44 | } while (m != -1) | |
| 45 | } | |
| 46 |     finally { stream.close }
 | |
| 47 | ||
| 48 | make_result(digest) | |
| 49 | } | |
| 50 | ||
| 51 | def digest(bytes: Array[Byte]): Digest = | |
| 52 |   {
 | |
| 53 |     val digest = MessageDigest.getInstance("SHA")
 | |
| 54 | digest.update(bytes) | |
| 55 | ||
| 56 | make_result(digest) | |
| 57 | } | |
| 58 | ||
| 50203 | 59 | def digest(string: String): Digest = digest(UTF8.string_bytes(string)) | 
| 38473 | 60 | } | 
| 61 |