src/Pure/General/sha1.scala
author wenzelm
Sun, 25 Nov 2012 20:17:04 +0100
changeset 50203 00d8ad713e32
parent 49696 3003c87f7814
child 54440 2c4940d2edf7
permissions -rw-r--r--
explicit module UTF8;
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
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48343
diff changeset
    11
import java.io.{File => JFile, FileInputStream}
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    12
import java.security.MessageDigest
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
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    15
object SHA1
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    16
{
43714
3749d1e6dde9 tuned signature;
wenzelm
parents: 41954
diff changeset
    17
  sealed case class Digest(rep: String)
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    18
  {
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    19
    override def toString: String = rep
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    20
  }
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    21
48343
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    22
  private def make_result(digest: MessageDigest): Digest =
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    23
  {
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    24
    val result = new StringBuilder
48343
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    25
    for (b <- digest.digest()) {
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    26
      val i = b.asInstanceOf[Int] & 0xFF
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    27
      if (i < 16) result += '0'
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    28
      result ++= Integer.toHexString(i)
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    29
    }
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    30
    Digest(result.toString)
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    31
  }
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    32
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48343
diff changeset
    33
  def digest(file: JFile): Digest =
48343
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    34
  {
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    35
    val stream = new FileInputStream(file)
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    36
    val digest = MessageDigest.getInstance("SHA")
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    37
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    38
    val buf = new Array[Byte](65536)
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    39
    var m = 0
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    40
    try {
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    41
      do {
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    42
        m = stream.read(buf, 0, buf.length)
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    43
        if (m != -1) digest.update(buf, 0, m)
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    44
      } while (m != -1)
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    45
    }
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    46
    finally { stream.close }
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    47
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    48
    make_result(digest)
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    49
  }
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    50
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    51
  def digest(bytes: Array[Byte]): Digest =
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    52
  {
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    53
    val digest = MessageDigest.getInstance("SHA")
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    54
    digest.update(bytes)
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    55
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    56
    make_result(digest)
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    57
  }
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    58
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 49696
diff changeset
    59
  def digest(string: String): Digest = digest(UTF8.string_bytes(string))
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    60
}
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    61