src/Pure/General/sha1.scala
author wenzelm
Mon, 28 Nov 2011 22:18:19 +0100
changeset 45667 546d78f0d81f
parent 43714 3749d1e6dde9
child 45673 cd41e3903fbf
permissions -rw-r--r--
explicit indication of modules for independent Scala library;
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
45667
546d78f0d81f explicit indication of modules for independent Scala library;
wenzelm
parents: 43714
diff changeset
     2
    Module:     Library
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
     4
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
     5
Digest strings according to SHA-1 (see RFC 3174).
38473
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
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
     8
package isabelle
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
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    11
import java.security.MessageDigest
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
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    14
object SHA1
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    15
{
43714
3749d1e6dde9 tuned signature;
wenzelm
parents: 41954
diff changeset
    16
  sealed case class Digest(rep: String)
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    17
  {
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    18
    override def toString: String = rep
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    19
  }
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    20
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    21
  def digest_bytes(bytes: Array[Byte]): Digest =
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    22
  {
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    23
    val result = new StringBuilder
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    24
    for (b <- MessageDigest.getInstance("SHA").digest(bytes)) {
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    25
      val i = b.asInstanceOf[Int] & 0xFF
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    26
      if (i < 16) result += '0'
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    27
      result ++= Integer.toHexString(i)
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    28
    }
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    29
    Digest(result.toString)
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    30
  }
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    31
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    32
  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
    33
}
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    34