author | wenzelm |
Mon, 06 Feb 2023 14:54:15 +0100 | |
changeset 77207 | d98a99e4eea9 |
parent 77204 | d69732bc3dbe |
child 77209 | 3070001c9d1f |
permissions | -rw-r--r-- |
38473 | 1 |
/* Title: Pure/General/sha1.scala |
2 |
Author: Makarius |
|
3 |
||
75309 | 4 |
SHA-1 message digest according to RFC 3174. |
38473 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
48409 | 10 |
import java.io.{File => JFile, FileInputStream} |
38473 | 11 |
import java.security.MessageDigest |
75309 | 12 |
|
13 |
import isabelle.setup.{Build => Setup_Build} |
|
38473 | 14 |
|
15 |
||
75393 | 16 |
object SHA1 { |
77207
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
17 |
/* digest */ |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
18 |
|
75393 | 19 |
final class Digest private[SHA1](rep: String) { |
75310 | 20 |
override def toString: String = rep |
55802
f7ceebe2f1b5
prefer abstract datatype -- in accordance to ML version;
wenzelm
parents:
54440
diff
changeset
|
21 |
override def hashCode: Int = rep.hashCode |
f7ceebe2f1b5
prefer abstract datatype -- in accordance to ML version;
wenzelm
parents:
54440
diff
changeset
|
22 |
override def equals(that: Any): Boolean = |
f7ceebe2f1b5
prefer abstract datatype -- in accordance to ML version;
wenzelm
parents:
54440
diff
changeset
|
23 |
that match { |
75310 | 24 |
case other: Digest => rep == other.toString |
55802
f7ceebe2f1b5
prefer abstract datatype -- in accordance to ML version;
wenzelm
parents:
54440
diff
changeset
|
25 |
case _ => false |
f7ceebe2f1b5
prefer abstract datatype -- in accordance to ML version;
wenzelm
parents:
54440
diff
changeset
|
26 |
} |
75348 | 27 |
def shasum(name: String): String = rep + " " + name |
41954 | 28 |
} |
29 |
||
75309 | 30 |
def fake_digest(rep: String): Digest = new Digest(rep) |
38473 | 31 |
|
75393 | 32 |
def make_digest(body: MessageDigest => Unit): Digest = { |
75309 | 33 |
val digest_body = new Setup_Build.Digest_Body { def apply(sha: MessageDigest): Unit = body(sha)} |
34 |
new Digest(Setup_Build.make_digest(digest_body)) |
|
35 |
} |
|
62702 | 36 |
|
48409 | 37 |
def digest(file: JFile): Digest = |
75394 | 38 |
make_digest(sha => using(new FileInputStream(file)) { stream => |
39 |
val buf = new Array[Byte](65536) |
|
40 |
var m = 0 |
|
75709 | 41 |
while ({ |
75394 | 42 |
m = stream.read(buf, 0, buf.length) |
43 |
if (m != -1) sha.update(buf, 0, m) |
|
75709 | 44 |
m != -1 |
45 |
}) () |
|
75394 | 46 |
}) |
48343 | 47 |
|
62704
478b49f0d726
proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;
wenzelm
parents:
62702
diff
changeset
|
48 |
def digest(path: Path): Digest = digest(path.file) |
75309 | 49 |
def digest(bytes: Array[Byte]): Digest = make_digest(_.update(bytes)) |
54440 | 50 |
def digest(bytes: Bytes): Digest = bytes.sha1_digest |
51 |
def digest(string: String): Digest = digest(Bytes(string)) |
|
72654 | 52 |
def digest_set(digests: List[Digest]): Digest = |
53 |
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
|
54 |
|
75310 | 55 |
val digest_length: Int = digest("").toString.length |
77204 | 56 |
|
77207
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
57 |
|
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
58 |
/* shasum */ |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
59 |
|
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
60 |
final class Shasum private[SHA1](private[SHA1] val rep: List[String]) { |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
61 |
override def equals(other: Any): Boolean = |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
62 |
other match { |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
63 |
case that: Shasum => rep.equals(that.rep) |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
64 |
case _ => false |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
65 |
} |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
66 |
override def hashCode: Int = rep.hashCode |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
67 |
override def toString: String = Library.terminate_lines(rep) |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
68 |
|
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
69 |
def is_empty: Boolean = rep.isEmpty |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
70 |
|
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
71 |
def digest: Digest = { |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
72 |
rep match { |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
73 |
case List(s) |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
74 |
if s.length == digest_length && s.forall(Symbol.is_ascii_hex) => fake_digest(s) |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
75 |
case _ => SHA1.digest(toString) |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
76 |
} |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
77 |
} |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
78 |
} |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
79 |
|
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
80 |
val no_shasum: Shasum = new Shasum(Nil) |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
81 |
def flat_shasum(list: List[Shasum]): Shasum = new Shasum(list.flatMap(_.rep)) |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
82 |
def fake_shasum(text: String): Shasum = new Shasum(Library.trim_split_lines(text)) |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
83 |
|
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
84 |
def shasum(digest: Digest, name: String): Shasum = new Shasum(List(digest.toString + " " + name)) |
d98a99e4eea9
proper Shasum.digest, to emulate old form from build_history database;
wenzelm
parents:
77204
diff
changeset
|
85 |
def shasum_meta_info(digest: Digest): Shasum = shasum(digest, isabelle.setup.Build.META_INFO) |
38473 | 86 |
} |