src/Tools/Setup/isabelle/setup/Build.java
author wenzelm
Fri, 09 Jul 2021 14:43:41 +0200
changeset 73954 a3a64aab815a
parent 73952 74ab1fb470a3
child 73955 2b9ae1aa9257
permissions -rw-r--r--
support mixed Scala/Java build; clarified scalac/javac options;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73944
3cee9d20308e clarified modules;
wenzelm
parents: 73931
diff changeset
     1
/*  Title:      Tools/Setup/isabelle/setup/Build.java
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
     3
73954
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
     4
Build Isabelle/Scala/Java modules.
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
     5
*/
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
     6
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
     7
package isabelle.setup;
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
     8
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
     9
73922
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
    10
import java.io.BufferedOutputStream;
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    11
import java.io.File;
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    12
import java.io.IOException;
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    13
import java.math.BigInteger;
73946
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
    14
import java.nio.charset.StandardCharsets;
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    15
import java.nio.file.Files;
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    16
import java.nio.file.Path;
73918
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
    17
import java.nio.file.StandardCopyOption;
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    18
import java.security.MessageDigest;
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    19
import java.security.NoSuchAlgorithmException;
73930
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
    20
import java.util.ArrayList;
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    21
import java.util.Comparator;
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    22
import java.util.LinkedList;
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    23
import java.util.List;
73919
429c1ffb5a36 proper treatment of leading zero;
wenzelm
parents: 73918
diff changeset
    24
import java.util.Locale;
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    25
import java.util.Properties;
73922
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
    26
import java.util.jar.Attributes;
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
    27
import java.util.jar.JarEntry;
73946
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
    28
import java.util.jar.JarFile;
73922
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
    29
import java.util.jar.JarOutputStream;
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
    30
import java.util.jar.Manifest;
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    31
import java.util.stream.Stream;
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    32
73954
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
    33
import javax.tools.JavaCompiler;
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
    34
import javax.tools.JavaFileObject;
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
    35
import javax.tools.StandardJavaFileManager;
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
    36
import javax.tools.ToolProvider;
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
    37
73930
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
    38
import scala.tools.nsc.MainClass;
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
    39
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    40
73944
3cee9d20308e clarified modules;
wenzelm
parents: 73931
diff changeset
    41
public class Build
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    42
{
73951
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    43
    /** context **/
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    44
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    45
    public static String BUILD_PROPS = "build.props";
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    46
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    47
    public static Context directory_context(Path dir)
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    48
        throws IOException
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    49
    {
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    50
        Properties props = new Properties();
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    51
        props.load(Files.newBufferedReader(dir.resolve(BUILD_PROPS)));
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    52
        return new Context(dir, props);
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    53
    }
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    54
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    55
    public static Context component_context(Path dir)
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    56
        throws IOException
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    57
    {
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    58
        Properties props = new Properties();
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    59
        Path build_props = dir.resolve("etc").resolve(BUILD_PROPS);
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    60
        if (Files.exists(build_props)) { props.load(Files.newBufferedReader(build_props)); }
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    61
        return new Context(dir, props);
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    62
    }
73922
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
    63
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    64
    public static class Context
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    65
    {
73951
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    66
        private final Path _dir;
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    67
        private final Properties _props;
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    68
73951
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    69
        public Context(Path dir, Properties props)
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    70
        {
73951
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    71
            _dir = dir;
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    72
            _props = props;
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    73
        }
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    74
73951
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    75
        @Override public String toString() { return _dir.toString(); }
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    76
73951
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    77
        public String name() { return _props.getProperty("name", _dir.toFile().getName()); }
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    78
        public String description() { return _props.getProperty("description", name()); }
73915
wenzelm
parents: 73914
diff changeset
    79
73951
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    80
        public String lib_name() { return _props.getProperty("lib", "lib") + "/" + name(); }
73917
b5d52a4d6fd9 tuned whitespace;
wenzelm
parents: 73916
diff changeset
    81
        public String jar_name() { return lib_name() + ".jar"; }
73915
wenzelm
parents: 73914
diff changeset
    82
73954
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
    83
        public String scalac_options() { return _props.getProperty("scalac_options", ""); }
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
    84
        public String javac_options() { return _props.getProperty("javac_options", ""); }
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
    85
73951
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    86
        public String main() { return _props.getProperty("main", ""); }
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
    87
73931
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
    88
        private List<String> get_list(String name)
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
    89
        {
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
    90
            List<String> list = new LinkedList<String>();
73951
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
    91
            for (String s : _props.getProperty(name, "").split("\\s+")) {
73931
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
    92
                if (!s.isEmpty()) { list.add(s); }
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
    93
            }
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
    94
            return List.copyOf(list);
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
    95
        }
73948
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
    96
        public List<String> requirements() { return get_list("requirements"); }
73931
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
    97
        public List<String> sources() { return get_list("sources"); }
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
    98
        public List<String> resources() { return get_list("resources"); }
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
    99
        public List<String> services() { return get_list("services"); }
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   100
73951
f209845d3a5d clarified signature;
wenzelm
parents: 73950
diff changeset
   101
        public Path path(String file) { return _dir.resolve(file); }
73917
b5d52a4d6fd9 tuned whitespace;
wenzelm
parents: 73916
diff changeset
   102
        public boolean exists(String file) { return Files.exists(path(file)); }
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   103
73946
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   104
        // historic
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   105
        public Path shasum_path() { return path(lib_name() + ".shasum"); }
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   106
73921
1f31ed84c467 tuned signature;
wenzelm
parents: 73920
diff changeset
   107
        public String item_name(String s)
73918
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   108
        {
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   109
            int i = s.indexOf(':');
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   110
            return i > 0 ? s.substring(0, i) : s;
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   111
        }
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   112
73921
1f31ed84c467 tuned signature;
wenzelm
parents: 73920
diff changeset
   113
        public String item_target(String s)
73918
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   114
        {
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   115
            int i = s.indexOf(':');
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   116
            return i > 0 ? s.substring(i + 1) : s;
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   117
        }
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   118
73948
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   119
        public String shasum(String name, List<Path> paths)
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   120
            throws IOException, NoSuchAlgorithmException
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   121
        {
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   122
            boolean exists = false;
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   123
            MessageDigest sha = MessageDigest.getInstance("SHA");
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   124
            for (Path file : paths) {
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   125
                if (Files.exists(file)) {
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   126
                    exists = true;
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   127
                    sha.update(Files.readAllBytes(file));
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   128
                }
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   129
            }
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   130
            if (exists) {
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   131
                String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest()));
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   132
                return digest + " " + name + "\n";
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   133
            }
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   134
            else { return ""; }
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   135
        }
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   136
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   137
        public String shasum(String file)
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   138
            throws IOException, NoSuchAlgorithmException
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   139
        {
73948
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   140
            return shasum(file, List.of(path(file)));
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   141
        }
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   142
    }
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   143
73922
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   144
73930
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   145
    /** compile sources **/
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   146
73954
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   147
    private static void add_options(List<String> options_list, String options)
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   148
    {
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   149
        if (options != null) {
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   150
            for (String s : options.split("\\s+")) {
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   151
                if (!s.isEmpty()) { options_list.add(s); }
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   152
            }
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   153
        }
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   154
    }
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   155
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   156
    public static void compile_scala_sources(
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   157
        Path target_dir, String more_options, List<Path> deps, List<Path> sources)
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   158
        throws IOException, InterruptedException
73930
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   159
    {
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   160
        ArrayList<String> args = new ArrayList<String>();
73954
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   161
        add_options(args, Environment.getenv("ISABELLE_SCALAC_OPTIONS"));
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   162
        add_options(args, more_options);
73930
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   163
        args.add("-d");
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   164
        args.add(target_dir.toString());
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   165
        args.add("-bootclasspath");
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   166
        args.add(Environment.join_paths(deps));
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   167
        args.add("--");
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   168
        for (Path p : sources) { args.add(p.toString()); }
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   169
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   170
        MainClass main = new MainClass();
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   171
        boolean ok = main.process(args.toArray(String[]::new));
73954
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   172
        if (!ok) throw new RuntimeException("Failed to compile Scala sources");
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   173
    }
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   174
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   175
    public static void compile_java_sources(
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   176
        Path target_dir, String more_options, List<Path> deps, List<Path> sources)
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   177
        throws IOException, InterruptedException
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   178
    {
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   179
        JavaCompiler compiler = ToolProvider.getSystemJavaCompiler();
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   180
        StandardJavaFileManager file_manager =
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   181
            compiler.getStandardFileManager(null, Locale.ROOT, StandardCharsets.UTF_8);
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   182
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   183
        List<String> options = new LinkedList<String>();
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   184
        add_options(options, Environment.getenv("ISABELLE_JAVAC_OPTIONS"));
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   185
        add_options(options, more_options);
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   186
        options.add("-d");
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   187
        options.add(target_dir.toString());
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   188
        options.add("-classpath");
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   189
        options.add(Environment.join_paths(deps));
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   190
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   191
        List<JavaFileObject> java_sources = new LinkedList<JavaFileObject>();
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   192
        for (Path p : sources) {
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   193
            if (p.toString().endsWith(".java")) {
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   194
                for (JavaFileObject o : file_manager.getJavaFileObjectsFromPaths(List.of(p))) {
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   195
                    java_sources.add(o);
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   196
                }
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   197
            }
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   198
        }
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   199
        if (!java_sources.isEmpty()) {
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   200
            boolean ok = compiler.getTask(null, file_manager, null, options, null, java_sources).call();
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   201
            if (!ok) throw new RuntimeException("Failed to compile Java sources");
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   202
        }
73930
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   203
    }
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   204
73922
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   205
73946
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   206
    /** shasum for jar content **/
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   207
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   208
    private static String SHASUM = "META-INF/shasum";
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   209
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   210
    public static String get_shasum(Path jar_path)
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   211
        throws IOException
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   212
    {
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   213
        if (Files.exists(jar_path)) {
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   214
            try (JarFile jar_file = new JarFile(jar_path.toFile()))
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   215
            {
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   216
                JarEntry entry = jar_file.getJarEntry(SHASUM);
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   217
                if (entry != null) {
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   218
                    byte[] bytes = jar_file.getInputStream(entry).readAllBytes();
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   219
                    return new String(bytes, StandardCharsets.UTF_8);
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   220
                }
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   221
                else { return ""; }
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   222
            }
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   223
        }
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   224
        else { return ""; }
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   225
    }
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   226
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   227
    public static void create_shasum(Path dir, String shasum)
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   228
        throws IOException
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   229
    {
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   230
        Path path = dir.resolve(SHASUM);
73948
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   231
        Files.createDirectories(path.getParent());
73946
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   232
        Files.writeString(path, shasum);
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   233
    }
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   234
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   235
73922
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   236
    /** create jar **/
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   237
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   238
    public static void create_jar(Path dir, String main, Path jar)
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   239
        throws IOException
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   240
    {
73949
714c267bb6fa more robust;
wenzelm
parents: 73948
diff changeset
   241
        Files.createDirectories(dir.resolve(jar).getParent());
73922
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   242
        Files.deleteIfExists(jar);
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   243
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   244
        Manifest manifest = new Manifest();
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   245
        Attributes attributes = manifest.getMainAttributes();
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   246
        attributes.put(Attributes.Name.MANIFEST_VERSION, "1.0");
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   247
        attributes.put(new Attributes.Name("Created-By"),
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   248
            System.getProperty("java.version") + " (" + System.getProperty("java.vendor") + ")");
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   249
        if (!main.isEmpty()) { attributes.put(Attributes.Name.MAIN_CLASS, main); }
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   250
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   251
        try (JarOutputStream out =
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   252
            new JarOutputStream(new BufferedOutputStream(Files.newOutputStream(jar)), manifest))
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   253
        {
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   254
            for (Path path : Files.walk(dir).sorted().toArray(Path[]::new)) {
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   255
                boolean is_dir = Files.isDirectory(path);
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   256
                boolean is_file = Files.isRegularFile(path);
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   257
                if (is_dir || is_file) {
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   258
                    String name = Environment.slashes(dir.relativize(path).toString());
73950
cc49da3003aa more robust;
wenzelm
parents: 73949
diff changeset
   259
                    if (!name.isEmpty()) {
cc49da3003aa more robust;
wenzelm
parents: 73949
diff changeset
   260
                        JarEntry entry = new JarEntry(is_dir ? name + "/" : name);
cc49da3003aa more robust;
wenzelm
parents: 73949
diff changeset
   261
                        entry.setTime(path.toFile().lastModified());
cc49da3003aa more robust;
wenzelm
parents: 73949
diff changeset
   262
                        out.putNextEntry(entry);
cc49da3003aa more robust;
wenzelm
parents: 73949
diff changeset
   263
                        if (is_file) { out.write(Files.readAllBytes(path)); }
cc49da3003aa more robust;
wenzelm
parents: 73949
diff changeset
   264
                        out.closeEntry();
cc49da3003aa more robust;
wenzelm
parents: 73949
diff changeset
   265
                    }
73922
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   266
                }
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   267
            }
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   268
        }
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   269
    }
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   270
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   271
73954
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   272
    /** build **/
73922
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   273
73954
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   274
    public static void build(Context context, boolean fresh)
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   275
        throws IOException, InterruptedException, NoSuchAlgorithmException
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   276
    {
73915
wenzelm
parents: 73914
diff changeset
   277
        String jar_name = context.jar_name();
73930
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   278
        Path jar_path = context.path(jar_name);
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   279
73948
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   280
        List<String> requirements = context.requirements();
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   281
        List<String> resources = context.resources();
73931
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
   282
        List<String> sources = context.sources();
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   283
73946
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   284
        Files.deleteIfExists(context.shasum_path());
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   285
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   286
        if (sources.isEmpty() && resources.isEmpty()) {
73930
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   287
            Files.deleteIfExists(jar_path);
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   288
        }
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   289
        else {
73946
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   290
            String shasum_old = get_shasum(jar_path);
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   291
            String shasum;
73948
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   292
            List<Path> compiler_deps = new LinkedList<Path>();
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   293
            {
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   294
                StringBuilder _shasum = new StringBuilder();
73948
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   295
                for (String s : requirements) {
73952
74ab1fb470a3 clarified syntax: similar to URL;
wenzelm
parents: 73951
diff changeset
   296
                    if (s.startsWith("env:")) {
73948
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   297
                        List<Path> paths = new LinkedList<Path>();
73952
74ab1fb470a3 clarified syntax: similar to URL;
wenzelm
parents: 73951
diff changeset
   298
                        for (String p : Environment.getenv(s.substring(4)).split(":", -1)) {
73948
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   299
                            if (!p.isEmpty()) {
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   300
                                Path path = Path.of(Environment.platform_path(p));
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   301
                                compiler_deps.add(path);
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   302
                                paths.add(path);
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   303
                            }
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   304
                        }
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   305
                        _shasum.append(context.shasum(s, paths));
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   306
                    }
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   307
                    else {
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   308
                        compiler_deps.add(context.path(s));
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   309
                        _shasum.append(context.shasum(s));
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   310
                    }
731ab64bae97 more compiler_deps via "requirements", notably jar list from settings;
wenzelm
parents: 73946
diff changeset
   311
                }
73918
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   312
                for (String s : resources) {
73921
1f31ed84c467 tuned signature;
wenzelm
parents: 73920
diff changeset
   313
                    _shasum.append(context.shasum(context.item_name(s)));
73918
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   314
                }
73920
3b340b44451c clarified order;
wenzelm
parents: 73919
diff changeset
   315
                for (String s : sources) { _shasum.append(context.shasum(s)); }
73946
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   316
                shasum = _shasum.toString();
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   317
            }
73946
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   318
            if (fresh || !shasum_old.equals(shasum)) {
73930
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   319
                System.out.println(
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   320
                    "### Building " + context.description() + " (" + jar_path + ") ...");
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   321
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   322
                String isabelle_class_path = Environment.getenv("ISABELLE_CLASSPATH");
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   323
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   324
                Path build_dir = Files.createTempDirectory("isabelle");
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   325
                try {
73930
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   326
                    /* compile sources */
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   327
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   328
                    for (String s : isabelle_class_path.split(":", -1)) {
73931
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
   329
                        if (!s.isEmpty()) {
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
   330
                          compiler_deps.add(Path.of(Environment.platform_path(s)));
4a708e150908 more robust treatment of empty string;
wenzelm
parents: 73930
diff changeset
   331
                        }
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   332
                    }
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   333
73930
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   334
                    List<Path> compiler_sources = new LinkedList<Path>();
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   335
                    for (String s : sources) { compiler_sources.add(context.path(s)); }
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   336
73954
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   337
                    compile_scala_sources(
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   338
                        build_dir, context.scalac_options(), compiler_deps, compiler_sources);
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   339
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   340
                    compiler_deps.add(build_dir);
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   341
                    compile_java_sources(
a3a64aab815a support mixed Scala/Java build;
wenzelm
parents: 73952
diff changeset
   342
                        build_dir, context.javac_options(), compiler_deps, compiler_sources);
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   343
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   344
73918
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   345
                    /* copy resources */
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   346
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   347
                    for (String s : context.resources()) {
73921
1f31ed84c467 tuned signature;
wenzelm
parents: 73920
diff changeset
   348
                        String name = context.item_name(s);
1f31ed84c467 tuned signature;
wenzelm
parents: 73920
diff changeset
   349
                        String target = context.item_target(s);
73918
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   350
                        Path file_name = Path.of(name).normalize().getFileName();
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   351
                        Path target_path = Path.of(target).normalize();
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   352
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   353
                        Path target_dir;
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   354
                        Path target_file;
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   355
                        {
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   356
                            if (target.endsWith("/") || target.endsWith("/.")) {
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   357
                                target_dir = build_dir.resolve(target_path);
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   358
                                target_file = target_dir.resolve(file_name);
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   359
                            }
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   360
                            else {
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   361
                                target_file = build_dir.resolve(target_path);
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   362
                                target_dir = target_file.getParent();
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   363
                            }
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   364
                        }
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   365
                        Files.createDirectories(target_dir);
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   366
                        Files.copy(context.path(name), target_file,
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   367
                            StandardCopyOption.COPY_ATTRIBUTES);
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   368
                    }
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   369
07781cae0f71 support for jar resources;
wenzelm
parents: 73917
diff changeset
   370
73922
3556303bd385 create jar in pure Java;
wenzelm
parents: 73921
diff changeset
   371
                    /* packaging */
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   372
73946
4d4c806cb7c8 clarified shasum: sources / resources within jar;
wenzelm
parents: 73944
diff changeset
   373
                    create_shasum(build_dir, shasum);
73930
17c09d1b3588 invoke Scala compiler from Java, without external process;
wenzelm
parents: 73922
diff changeset
   374
                    create_jar(build_dir, context.main(), jar_path);
73914
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   375
                }
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   376
                finally {
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   377
                    try (Stream<Path> walk = Files.walk(build_dir)) {
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   378
                        walk.sorted(Comparator.reverseOrder())
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   379
                            .map(Path::toFile)
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   380
                            .forEach(File::delete);
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   381
                    }
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   382
                }
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   383
            }
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   384
        }
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   385
    }
4be1047576e6 support for Isabelle/Scala in pure Java;
wenzelm
parents:
diff changeset
   386
}