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