# HG changeset patch
# User wenzelm
# Date 1626030041 -7200
# Node ID f6862d5f4e7fca1a1bedd5de2f93fd1b39bd63d7
# Parent  c9771e1b3223ea4f9dd1d3d448ae1030493d2f73
clarified Isabelle meta-info within jar;

diff -r c9771e1b3223 -r f6862d5f4e7f src/Tools/Setup/isabelle/setup/Build.java
--- a/src/Tools/Setup/isabelle/setup/Build.java	Sun Jul 11 20:47:55 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build.java	Sun Jul 11 21:00:41 2021 +0200
@@ -114,6 +114,11 @@
         public List<String> resources() { return get_list("resources"); }
         public List<String> services() { return get_list("services"); }
 
+        public boolean is_vacuous()
+        {
+            return sources().isEmpty() && resources().isEmpty() && services().isEmpty();
+        }
+
         public Path path(String file)
             throws IOException, InterruptedException
         {
@@ -243,7 +248,7 @@
 
     /** shasum for jar content **/
 
-    private static String SHASUM = "META-INF/shasum";
+    private static String SHASUM = "META-INF/isabelle/shasum";
 
     public static String get_shasum(Path jar_path)
         throws IOException
@@ -271,6 +276,38 @@
     }
 
 
+    /** services **/
+
+    private static String SERVICES = "META-INF/isabelle/services";
+
+    public static List<String> get_services(Path jar_path)
+        throws IOException
+    {
+        if (Files.exists(jar_path)) {
+            try (JarFile jar_file = new JarFile(jar_path.toFile()))
+            {
+                JarEntry entry = jar_file.getJarEntry(SERVICES);
+                if (entry != null) {
+                    byte[] bytes = jar_file.getInputStream(entry).readAllBytes();
+                    return Library.split_lines(new String(bytes, StandardCharsets.UTF_8));
+                }
+                else { return List.of(); }
+            }
+        }
+        else { return List.of(); }
+    }
+
+    public static void create_services(Path dir, List<String> services)
+        throws IOException
+    {
+        if (!services.isEmpty()) {
+            Path path = dir.resolve(SERVICES);
+            Files.createDirectories(path.getParent());
+            Files.writeString(path, Library.cat_lines(services));
+        }
+    }
+
+
     /** create jar **/
 
     public static void create_jar(Path dir, String main, Path jar)
@@ -346,9 +383,7 @@
 
         Files.deleteIfExists(context.shasum_path());
 
-        if (sources.isEmpty() && resources.isEmpty()) {
-            Files.deleteIfExists(jar_path);
-        }
+        if (context.is_vacuous()) { Files.deleteIfExists(jar_path); }
         else {
             String shasum_old = get_shasum(jar_path);
             String shasum;
@@ -434,6 +469,7 @@
                     /* packaging */
 
                     create_shasum(build_dir, shasum);
+                    create_services(build_dir, context.services());
                     create_jar(build_dir, context.main(), jar_path);
                 }
                 finally {