src/Pure/General/sha1.scala
author wenzelm
Mon, 08 Aug 2011 17:23:15 +0200
changeset 44058 ae85c5d64913
parent 43714 3749d1e6dde9
child 45667 546d78f0d81f
permissions -rw-r--r--
misc tuning -- eliminated old-fashioned rep_thm;

/*  Title:      Pure/General/sha1.scala
    Author:     Makarius

Digest strings according to SHA-1 (see RFC 3174).
*/

package isabelle


import java.security.MessageDigest


object SHA1
{
  sealed case class Digest(rep: String)
  {
    override def toString: String = rep
  }

  def digest_bytes(bytes: Array[Byte]): Digest =
  {
    val result = new StringBuilder
    for (b <- MessageDigest.getInstance("SHA").digest(bytes)) {
      val i = b.asInstanceOf[Int] & 0xFF
      if (i < 16) result += '0'
      result ++= Integer.toHexString(i)
    }
    Digest(result.toString)
  }

  def digest(s: String): Digest = digest_bytes(Standard_System.string_bytes(s))
}