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 digest = MessageDigest.getInstance("SHA") 43 44 using(new FileInputStream(file))(stream => 45 { 46 val buf = new Array[Byte](65536) 47 var m = 0 48 try { 49 do { 50 m = stream.read(buf, 0, buf.length) 51 if (m != -1) digest.update(buf, 0, m) 52 } while (m != -1) 53 } 54 }) 55 56 make_result(digest) 57 } 58 59 def digest(path: Path): Digest = digest(path.file) 60 61 def digest(bytes: Array[Byte]): Digest = 62 { 63 val digest = MessageDigest.getInstance("SHA") 64 digest.update(bytes) 65 66 make_result(digest) 67 } 68 69 def digest(bytes: Bytes): Digest = bytes.sha1_digest 70 def digest(string: String): Digest = digest(Bytes(string)) 71 72 val digest_length: Int = digest("").rep.length 73} 74