--- a/Admin/components/components.sha1 Wed Mar 23 11:40:34 2022 +0100
+++ b/Admin/components/components.sha1 Wed Mar 23 12:02:56 2022 +0100
@@ -148,6 +148,7 @@
309909ec6d43ae460338e9af54c1b2a48adcb1ec isabelle_setup-20210726.tar.gz
a14ce46c62c64c3413f3cc9239242e33570d0f3d isabelle_setup-20210922.tar.gz
b22066a9dcde6f813352dcf6404ac184440a22df isabelle_setup-20211109.tar.gz
+91c5d29e9fa40aee015e8e65ffea043e218c2fc5 isabelle_setup-20220323.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
--- a/Admin/components/main Wed Mar 23 11:40:34 2022 +0100
+++ b/Admin/components/main Wed Mar 23 12:02:56 2022 +0100
@@ -9,7 +9,7 @@
flatlaf-1.6.4
idea-icons-20210508
isabelle_fonts-20211004
-isabelle_setup-20211109
+isabelle_setup-20220323
jdk-17.0.2+8
jedit-20211103
jfreechart-1.5.3
--- a/src/Pure/General/sha1.scala Wed Mar 23 11:40:34 2022 +0100
+++ b/src/Pure/General/sha1.scala Wed Mar 23 12:02:56 2022 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/General/sha1.scala
Author: Makarius
-Digest strings according to SHA-1 (see RFC 3174).
+SHA-1 message digest according to RFC 3174.
*/
package isabelle
@@ -9,8 +9,8 @@
import java.io.{File => JFile, FileInputStream}
import java.security.MessageDigest
-import java.util.Locale
-import java.math.BigInteger
+
+import isabelle.setup.{Build => Setup_Build}
object SHA1
@@ -26,38 +26,27 @@
override def toString: String = rep
}
- private def sha1_digest(sha: MessageDigest): Digest =
- new Digest(String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest())))
+ def fake_digest(rep: String): Digest = new Digest(rep)
- def fake(rep: String): Digest = new Digest(rep)
+ def make_digest(body: MessageDigest => Unit): Digest =
+ {
+ val digest_body = new Setup_Build.Digest_Body { def apply(sha: MessageDigest): Unit = body(sha)}
+ new Digest(Setup_Build.make_digest(digest_body))
+ }
def digest(file: JFile): Digest =
- {
- val digest = MessageDigest.getInstance("SHA")
-
- using(new FileInputStream(file))(stream =>
- {
- val buf = new Array[Byte](65536)
- var m = 0
- do {
- m = stream.read(buf, 0, buf.length)
- if (m != -1) digest.update(buf, 0, m)
- } while (m != -1)
- })
-
- sha1_digest(digest)
- }
+ make_digest(sha => using(new FileInputStream(file))(stream =>
+ {
+ val buf = new Array[Byte](65536)
+ var m = 0
+ do {
+ m = stream.read(buf, 0, buf.length)
+ if (m != -1) sha.update(buf, 0, m)
+ } while (m != -1)
+ }))
def digest(path: Path): Digest = digest(path.file)
-
- def digest(bytes: Array[Byte]): Digest =
- {
- val digest = MessageDigest.getInstance("SHA")
- digest.update(bytes)
-
- sha1_digest(digest)
- }
-
+ def digest(bytes: Array[Byte]): Digest = make_digest(_.update(bytes))
def digest(bytes: Bytes): Digest = bytes.sha1_digest
def digest(string: String): Digest = digest(Bytes(string))
def digest_set(digests: List[Digest]): Digest =
--- a/src/Pure/Thy/document_build.scala Wed Mar 23 11:40:34 2022 +0100
+++ b/src/Pure/Thy/document_build.scala Wed Mar 23 12:02:56 2022 +0100
@@ -81,7 +81,7 @@
{
val name = res.string(Data.name)
val sources = res.string(Data.sources)
- Document_Input(name, SHA1.fake(sources))
+ Document_Input(name, SHA1.fake_digest(sources))
}).toList)
}
@@ -96,7 +96,7 @@
val sources = res.string(Data.sources)
val log_xz = res.bytes(Data.log_xz)
val pdf = res.bytes(Data.pdf)
- Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf))
+ Some(Document_Output(name, SHA1.fake_digest(sources), log_xz, pdf))
}
else None
})
--- a/src/Tools/Setup/src/Build.java Wed Mar 23 11:40:34 2022 +0100
+++ b/src/Tools/Setup/src/Build.java Wed Mar 23 12:02:56 2022 +0100
@@ -8,7 +8,6 @@
import java.io.BufferedOutputStream;
-import java.io.ByteArrayOutputStream;
import java.io.CharArrayWriter;
import java.io.File;
import java.io.IOException;
@@ -44,6 +43,30 @@
public class Build
{
+ /** SHA1 digest **/
+
+ @FunctionalInterface
+ public interface Digest_Body
+ {
+ void apply(MessageDigest sha) throws IOException, InterruptedException;
+ }
+
+ public static String make_digest(Digest_Body body)
+ throws NoSuchAlgorithmException, IOException, InterruptedException
+ {
+ MessageDigest sha = MessageDigest.getInstance("SHA");
+ body.apply(sha);
+ return String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest()));
+ }
+
+ public static String make_shasum(String name, Digest_Body body)
+ throws NoSuchAlgorithmException, IOException, InterruptedException
+ {
+ return make_digest(body) + " " + name + "\n";
+ }
+
+
+
/** context **/
public static String BUILD_PROPS = "build.props";
@@ -77,12 +100,6 @@
return List.copyOf(result);
}
- private static String sha_digest(MessageDigest sha, String name)
- {
- String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest()));
- return digest + " " + name + "\n";
- }
-
public static class Context
{
private final Path _dir;
@@ -181,37 +198,37 @@
}
public String shasum(String name, List<Path> paths)
- throws IOException, NoSuchAlgorithmException
+ throws NoSuchAlgorithmException, IOException, InterruptedException
{
- MessageDigest sha = MessageDigest.getInstance("SHA");
- for (Path file : paths) {
- if (Files.isRegularFile(file)) {
- sha.update(Files.readAllBytes(file));
- }
- else {
- throw new RuntimeException(
- error_message("Bad input file " + Library.quote(file.toString())));
- }
- }
- return sha_digest(sha, name);
+ return make_shasum(name, sha ->
+ {
+ for (Path file : paths) {
+ if (Files.isRegularFile(file)) {
+ sha.update(Files.readAllBytes(file));
+ }
+ else {
+ throw new RuntimeException(
+ error_message("Bad input file " + Library.quote(file.toString())));
+ }
+ }
+ });
}
public String shasum(String file)
- throws IOException, NoSuchAlgorithmException, InterruptedException
+ throws NoSuchAlgorithmException, IOException, InterruptedException
{
return shasum(file, List.of(path(file)));
}
public String shasum_props()
- throws NoSuchAlgorithmException
+ throws NoSuchAlgorithmException, IOException, InterruptedException
{
TreeMap<String,Object> sorted = new TreeMap<String,Object>();
for (Object x : _props.entrySet()) {
sorted.put(x.toString(), _props.get(x));
}
- MessageDigest sha = MessageDigest.getInstance("SHA");
- sha.update(sorted.toString().getBytes(StandardCharsets.UTF_8));
- return sha_digest(sha, "<props>");
+ return make_shasum("<props>",
+ sha -> sha.update(sorted.toString().getBytes(StandardCharsets.UTF_8)));
}
}
@@ -423,7 +440,7 @@
/** build **/
public static void build(PrintStream output, Context context, boolean fresh)
- throws IOException, InterruptedException, NoSuchAlgorithmException
+ throws NoSuchAlgorithmException, IOException, InterruptedException
{
String module = context.module_result();
if (!module.isEmpty()) {
@@ -532,7 +549,7 @@
}
public static void build_components(PrintStream output, boolean fresh)
- throws IOException, InterruptedException, NoSuchAlgorithmException
+ throws NoSuchAlgorithmException, IOException, InterruptedException
{
for (Context context : component_contexts()) {
build(output, context, fresh);