src/Pure/General/sha1.scala
author wenzelm
Tue, 29 Nov 2011 21:29:53 +0100
changeset 45673 cd41e3903fbf
parent 45667 546d78f0d81f
child 48343 3060e6343953
permissions -rw-r--r--
separate compilation of PIDE vs. Pure sources, which enables 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
45673
cd41e3903fbf separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents: 45667
diff changeset
     2
    Module:     PIDE
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