src/Pure/General/sha1.scala
author wenzelm
Fri, 01 Apr 2022 17:06:10 +0200
changeset 75393 87ebf5a50283
parent 75382 81673c441ce3
child 75394 42267c650205
permissions -rw-r--r--
clarified formatting, for the sake of scala3;
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
75309
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
     4
SHA-1 message digest according to 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
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48343
diff changeset
    10
import java.io.{File => JFile, FileInputStream}
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    11
import java.security.MessageDigest
75309
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
    12
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
    13
import isabelle.setup.{Build => Setup_Build}
38473
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
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
    16
object SHA1 {
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
    17
  final class Digest private[SHA1](rep: String) {
75310
42baf7ffa088 tuned signature;
wenzelm
parents: 75309
diff changeset
    18
    override def toString: String = rep
55802
f7ceebe2f1b5 prefer abstract datatype -- in accordance to ML version;
wenzelm
parents: 54440
diff changeset
    19
    override def hashCode: Int = rep.hashCode
f7ceebe2f1b5 prefer abstract datatype -- in accordance to ML version;
wenzelm
parents: 54440
diff changeset
    20
    override def equals(that: Any): Boolean =
f7ceebe2f1b5 prefer abstract datatype -- in accordance to ML version;
wenzelm
parents: 54440
diff changeset
    21
      that match {
75310
42baf7ffa088 tuned signature;
wenzelm
parents: 75309
diff changeset
    22
        case other: Digest => rep == other.toString
55802
f7ceebe2f1b5 prefer abstract datatype -- in accordance to ML version;
wenzelm
parents: 54440
diff changeset
    23
        case _ => false
f7ceebe2f1b5 prefer abstract datatype -- in accordance to ML version;
wenzelm
parents: 54440
diff changeset
    24
      }
75348
583ad7a9941c tuned signature;
wenzelm
parents: 75310
diff changeset
    25
    def shasum(name: String): String = rep + " " + name
41954
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    26
  }
fb94df4505a0 explicit type SHA1.digest;
wenzelm
parents: 38473
diff changeset
    27
75309
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
    28
  def fake_digest(rep: String): Digest = new Digest(rep)
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    29
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
    30
  def make_digest(body: MessageDigest => Unit): Digest = {
75309
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
    31
    val digest_body = new Setup_Build.Digest_Body { def apply(sha: MessageDigest): Unit = body(sha)}
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
    32
    new Digest(Setup_Build.make_digest(digest_body))
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
    33
  }
62702
e29f47e04180 tuned signature;
wenzelm
parents: 57638
diff changeset
    34
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48343
diff changeset
    35
  def digest(file: JFile): Digest =
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75382
diff changeset
    36
    make_digest(sha => using(new FileInputStream(file))(stream => {
75309
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
    37
        val buf = new Array[Byte](65536)
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
    38
        var m = 0
75382
81673c441ce3 tuned: eliminted do-while for the sake of scala3;
wenzelm
parents: 75348
diff changeset
    39
        var cont = true
81673c441ce3 tuned: eliminted do-while for the sake of scala3;
wenzelm
parents: 75348
diff changeset
    40
        while (cont) {
75309
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
    41
          m = stream.read(buf, 0, buf.length)
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
    42
          if (m != -1) sha.update(buf, 0, m)
75382
81673c441ce3 tuned: eliminted do-while for the sake of scala3;
wenzelm
parents: 75348
diff changeset
    43
          cont = (m != -1)
81673c441ce3 tuned: eliminted do-while for the sake of scala3;
wenzelm
parents: 75348
diff changeset
    44
        }
75309
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
    45
      }))
48343
3060e6343953 more SHA1.digest operations;
wenzelm
parents: 45673
diff changeset
    46
62704
478b49f0d726 proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents: 62702
diff changeset
    47
  def digest(path: Path): Digest = digest(path.file)
75309
216c2ac23a84 clarified signature;
wenzelm
parents: 75307
diff changeset
    48
  def digest(bytes: Array[Byte]): Digest = make_digest(_.update(bytes))
54440
2c4940d2edf7 tuned signature;
wenzelm
parents: 50203
diff changeset
    49
  def digest(bytes: Bytes): Digest = bytes.sha1_digest
2c4940d2edf7 tuned signature;
wenzelm
parents: 50203
diff changeset
    50
  def digest(string: String): Digest = digest(Bytes(string))
72654
99a6bcd1e8e4 tuned signature;
wenzelm
parents: 71775
diff changeset
    51
  def digest_set(digests: List[Digest]): Digest =
99a6bcd1e8e4 tuned signature;
wenzelm
parents: 71775
diff changeset
    52
    digest(cat_lines(digests.map(_.toString).sorted))
57638
ed58e740a699 less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
wenzelm
parents: 55802
diff changeset
    53
75310
42baf7ffa088 tuned signature;
wenzelm
parents: 75309
diff changeset
    54
  val digest_length: Int = digest("").toString.length
38473
bd96f2a5beb0 digesting strings according to SHA-1 -- Scala version;
wenzelm
parents:
diff changeset
    55
}