# HG changeset patch
# User wenzelm
# Date 1625746836 -7200
# Node ID 4d4c806cb7c8ce57babfd3e3133842eabab85dc9
# Parent  e61add9d5b5e31752e5e3d078014994c14c57f74
clarified shasum: sources / resources within jar;

diff -r e61add9d5b5e -r 4d4c806cb7c8 src/Tools/Setup/isabelle/setup/Build.java
--- a/src/Tools/Setup/isabelle/setup/Build.java	Thu Jul 08 13:34:12 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build.java	Thu Jul 08 14:20:36 2021 +0200
@@ -11,6 +11,7 @@
 import java.io.File;
 import java.io.IOException;
 import java.math.BigInteger;
+import java.nio.charset.StandardCharsets;
 import java.nio.file.Files;
 import java.nio.file.Path;
 import java.nio.file.StandardCopyOption;
@@ -24,6 +25,7 @@
 import java.util.Properties;
 import java.util.jar.Attributes;
 import java.util.jar.JarEntry;
+import java.util.jar.JarFile;
 import java.util.jar.JarOutputStream;
 import java.util.jar.Manifest;
 import java.util.stream.Stream;
@@ -56,7 +58,6 @@
 
         public String lib_name() { return props.getProperty("lib", "lib") + "/" + name(); }
         public String jar_name() { return lib_name() + ".jar"; }
-        public String shasum_name() { return lib_name() + ".shasum"; }
 
         public String main() { return props.getProperty("main", ""); }
 
@@ -75,6 +76,9 @@
         public Path path(String file) { return component_dir.resolve(file); }
         public boolean exists(String file) { return Files.exists(path(file)); }
 
+        // historic
+        public Path shasum_path() { return path(lib_name() + ".shasum"); }
+
         public String item_name(String s)
         {
             int i = s.indexOf(':');
@@ -94,7 +98,7 @@
                 MessageDigest sha = MessageDigest.getInstance("SHA");
                 sha.update(Files.readAllBytes(path(file)));
                 String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest()));
-                return digest + " *" + file + "\n";
+                return digest + " " + file + "\n";
             }
             else { return ""; }
         }
@@ -123,6 +127,36 @@
     }
 
 
+    /** shasum for jar content **/
+
+    private static String SHASUM = "META-INF/shasum";
+
+    public static String get_shasum(Path jar_path)
+        throws IOException
+    {
+        if (Files.exists(jar_path)) {
+            try (JarFile jar_file = new JarFile(jar_path.toFile()))
+            {
+                JarEntry entry = jar_file.getJarEntry(SHASUM);
+                if (entry != null) {
+                    byte[] bytes = jar_file.getInputStream(entry).readAllBytes();
+                    return new String(bytes, StandardCharsets.UTF_8);
+                }
+                else { return ""; }
+            }
+        }
+        else { return ""; }
+    }
+
+    public static void create_shasum(Path dir, String shasum)
+        throws IOException
+    {
+        Path path = dir.resolve(SHASUM);
+        Files.createDirectories(dir.getParent());
+        Files.writeString(path, shasum);
+    }
+
+
     /** create jar **/
 
     public static void create_jar(Path dir, String main, Path jar)
@@ -164,28 +198,27 @@
     {
         String jar_name = context.jar_name();
         Path jar_path = context.path(jar_name);
-        String shasum_name = context.shasum_name();
 
         List<String> sources = context.sources();
         List<String> resources = context.resources();
 
-        if (sources.isEmpty()) {
+        Files.deleteIfExists(context.shasum_path());
+
+        if (sources.isEmpty() && resources.isEmpty()) {
             Files.deleteIfExists(jar_path);
-            Files.deleteIfExists(context.path(shasum_name));
         }
         else {
-            String shasum_old =
-                context.exists(shasum_name) ? Files.readString(context.path(shasum_name)) : "";
-            String shasum_sources;
+            String shasum_old = get_shasum(jar_path);
+            String shasum;
             {
                 StringBuilder _shasum = new StringBuilder();
                 for (String s : resources) {
                     _shasum.append(context.shasum(context.item_name(s)));
                 }
                 for (String s : sources) { _shasum.append(context.shasum(s)); }
-                shasum_sources = _shasum.toString();
+                shasum = _shasum.toString();
             }
-            if (fresh || !shasum_old.equals(context.shasum(jar_name) + shasum_sources)) {
+            if (fresh || !shasum_old.equals(shasum)) {
                 System.out.println(
                     "### Building " + context.description() + " (" + jar_path + ") ...");
 
@@ -237,10 +270,8 @@
 
                     /* packaging */
 
+                    create_shasum(build_dir, shasum);
                     create_jar(build_dir, context.main(), jar_path);
-
-                    String shasum = context.shasum(jar_name) + shasum_sources;
-                    Files.writeString(context.path(shasum_name), shasum);
                 }
                 finally {
                     try (Stream<Path> walk = Files.walk(build_dir)) {