1/* Title: Pure/General/sha1.scala 2 Author: Makarius 3 4Digest strings according to SHA-1 (see RFC 3174). 5*/ 6 7package isabelle 8 9 10import java.io.{File => JFile, FileInputStream} 11import java.security.MessageDigest 12 13 14object SHA1 15{ 16 final class Digest private[SHA1](val rep: String) 17 { 18 override def hashCode: Int = rep.hashCode 19 override def equals(that: Any): Boolean = 20 that match { 21 case other: Digest => rep == other.rep 22 case _ => false 23 } 24 override def toString: String = rep 25 } 26 27 private def make_result(digest: MessageDigest): Digest = 28 { 29 val result = new StringBuilder 30 for (b <- digest.digest()) { 31 val i = b.asInstanceOf[Int] & 0xFF 32 if (i < 16) result += '0' 33 result ++= Integer.toHexString(i) 34 } 35 new Digest(result.toString) 36 } 37 38 def fake(rep: String): Digest = new Digest(rep) 39 40 def digest(file: JFile): Digest = 41 { 42 val stream = new FileInputStream(file) 43 val digest = MessageDigest.getInstance("SHA") 44 45 val buf = new Array[Byte](65536) 46 var m = 0 47 try { 48 do { 49 m = stream.read(buf, 0, buf.length) 50 if (m != -1) digest.update(buf, 0, m) 51 } while (m != -1) 52 } 53 finally { stream.close } 54 55 make_result(digest) 56 } 57 58 def digest(path: Path): Digest = digest(path.file) 59 60 def digest(bytes: Array[Byte]): Digest = 61 { 62 val digest = MessageDigest.getInstance("SHA") 63 digest.update(bytes) 64 65 make_result(digest) 66 } 67 68 def digest(bytes: Bytes): Digest = bytes.sha1_digest 69 def digest(string: String): Digest = digest(Bytes(string)) 70 71 val digest_length: Int = digest("").rep.length 72} 73