src/Pure/General/sha1.scala
author wenzelm
Wed, 29 Dec 2010 20:41:33 +0100
changeset 41415 23533273220a
parent 38473 bd96f2a5beb0
child 41954 fb94df4505a0
permissions -rw-r--r--
tuned ML toplevel pp for type string: observe depth limit;
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
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
     4
Digesting strings according to SHA-1 (see RFC 3174).
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
{
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    15
  def digest_bytes(bytes: Array[Byte]): String =
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    16
  {
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    17
    val result = new StringBuilder
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    18
    for (b <- MessageDigest.getInstance("SHA").digest(bytes)) {
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    19
      val i = b.asInstanceOf[Int] & 0xFF
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    20
      if (i < 16) result += '0'
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    21
      result ++= Integer.toHexString(i)
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
    result.toString
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    24
  }
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    25
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    26
  def digest(s: String): String = digest_bytes(Standard_System.string_bytes(s))
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    27
}
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    28