# HG changeset patch
# User wenzelm
# Date 1625227725 -7200
# Node ID 3556303bd38553d37d1a51e9b5d3ba219ad58652
# Parent  1f31ed84c46798fc37cd784c462c5a32e527c972
create jar in pure Java;

diff -r 1f31ed84c467 -r 3556303bd385 src/Tools/Setup/isabelle/setup/Build_Scala.java
--- a/src/Tools/Setup/isabelle/setup/Build_Scala.java	Fri Jul 02 12:23:42 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build_Scala.java	Fri Jul 02 14:08:45 2021 +0200
@@ -7,8 +7,10 @@
 package isabelle.setup;
 
 
+import java.io.BufferedOutputStream;
 import java.io.File;
 import java.io.IOException;
+import java.io.OutputStream;
 import java.math.BigInteger;
 import java.nio.file.Files;
 import java.nio.file.Path;
@@ -22,11 +24,17 @@
 import java.util.Locale;
 import java.util.Map;
 import java.util.Properties;
+import java.util.jar.Attributes;
+import java.util.jar.JarEntry;
+import java.util.jar.JarOutputStream;
+import java.util.jar.Manifest;
 import java.util.stream.Stream;
 
 
 public class Build_Scala
 {
+    /** component directory context **/
+
     public static class Context
     {
         private final Path component_dir;
@@ -84,6 +92,44 @@
         }
     }
 
+
+
+    /** create jar **/
+
+    public static void create_jar(Path dir, String main, Path jar)
+        throws IOException
+    {
+        Files.deleteIfExists(jar);
+
+        Manifest manifest = new Manifest();
+        Attributes attributes = manifest.getMainAttributes();
+        attributes.put(Attributes.Name.MANIFEST_VERSION, "1.0");
+        attributes.put(new Attributes.Name("Created-By"),
+            System.getProperty("java.version") + " (" + System.getProperty("java.vendor") + ")");
+        if (!main.isEmpty()) { attributes.put(Attributes.Name.MAIN_CLASS, main); }
+
+        try (JarOutputStream out =
+            new JarOutputStream(new BufferedOutputStream(Files.newOutputStream(jar)), manifest))
+        {
+            for (Path path : Files.walk(dir).sorted().toArray(Path[]::new)) {
+                boolean is_dir = Files.isDirectory(path);
+                boolean is_file = Files.isRegularFile(path);
+                if (is_dir || is_file) {
+                    String name = Environment.slashes(dir.relativize(path).toString());
+                    JarEntry entry = new JarEntry(is_dir ? name + "/" : name);
+                    entry.setTime(path.toFile().lastModified());
+                    out.putNextEntry(entry);
+                    if (is_file) { out.write(Files.readAllBytes(path)); }
+                    out.closeEntry();
+                }
+            }
+        }
+    }
+
+
+
+    /** build scala **/
+
     public static void build_scala(Context context, boolean fresh)
         throws IOException, InterruptedException, NoSuchAlgorithmException
     {
@@ -178,24 +224,9 @@
                     }
 
 
-                    /* jar */
+                    /* packaging */
 
-                    cmd.clear();
-                    cmd.add(Environment.platform_path(java_home + "/bin/jar"));
-                    cmd.add("-c");
-                    cmd.add("-f");
-                    cmd.add(context.path(jar_name).toString());
-                    if (!context.main().isEmpty()) {
-                        cmd.add("-e");
-                        cmd.add(context.main());
-                    }
-                    cmd.add(".");
-
-                    res = Environment.exec_process(cmd, build_dir.toFile(), env, false);
-                    if (!res.ok()) throw new RuntimeException(res.err());
-
-
-                    /* shasum */
+                    create_jar(build_dir, context.main(), context.path(jar_name));
 
                     String shasum = context.shasum(jar_name) + shasum_sources;
                     Files.writeString(context.path(shasum_name), shasum);
diff -r 1f31ed84c467 -r 3556303bd385 src/Tools/Setup/isabelle/setup/Environment.java
--- a/src/Tools/Setup/isabelle/setup/Environment.java	Fri Jul 02 12:23:42 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Environment.java	Fri Jul 02 14:08:45 2021 +0200
@@ -39,7 +39,7 @@
 
     /* system path representations */
 
-    private static String slashes(String s) { return s.replace('\\', '/'); }
+    public static String slashes(String s) { return s.replace('\\', '/'); }
 
     public static String standard_path(String cygwin_root, String platform_path)
     {