src/Pure/General/sha1.scala
author wenzelm
Sat, 09 Jul 2011 12:56:51 +0200
changeset 43714 3749d1e6dde9
parent 41954 fb94df4505a0
child 45667 546d78f0d81f
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/sha1.scala
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
     3
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
     4
Digest strings according to SHA-1 (see RFC 3174).
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
     5
*/
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
     6
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
     7
package isabelle
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
     8
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
     9
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    10
import java.security.MessageDigest
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    11
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    12
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    13
object SHA1
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    14
{
43714
3749d1e6dde9 tuned signature;
wenzelm
parents: 41954
diff changeset
    15
  sealed case class Digest(rep: String)
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    16
  {
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    17
    override def toString: String = rep
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    18
  }
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    19
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    20
  def digest_bytes(bytes: Array[Byte]): Digest =
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    21
  {
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    22
    val result = new StringBuilder
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    23
    for (b <- MessageDigest.getInstance("SHA").digest(bytes)) {
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    24
      val i = b.asInstanceOf[Int] & 0xFF
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    25
      if (i < 16) result += '0'
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    26
      result ++= Integer.toHexString(i)
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    27
    }
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    28
    Digest(result.toString)
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    29
  }
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    30
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    31
  def digest(s: String): Digest = digest_bytes(Standard_System.string_bytes(s))
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    32
}
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    33