clarified directories;
authorwenzelm
Sat, 17 Jul 2021 21:40:57 +0200
changeset 74295 09821ca262d3
parent 74294 39e05601faeb
child 74296 c9ec6f03ab91
clarified directories;
Admin/lib/Tools/build_setup
src/Tools/Setup/isabelle/setup/Build.java
src/Tools/Setup/isabelle/setup/Environment.java
src/Tools/Setup/isabelle/setup/Exn.java
src/Tools/Setup/isabelle/setup/Library.java
src/Tools/Setup/isabelle/setup/Setup.java
src/Tools/Setup/src/Build.java
src/Tools/Setup/src/Environment.java
src/Tools/Setup/src/Exn.java
src/Tools/Setup/src/Library.java
src/Tools/Setup/src/Setup.java
--- a/Admin/lib/Tools/build_setup	Sat Jul 17 21:31:15 2021 +0200
+++ b/Admin/lib/Tools/build_setup	Sat Jul 17 21:40:57 2021 +0200
@@ -73,8 +73,8 @@
 
 for SRC in "${SOURCES[@]}"
 do
-  ARGS["${#ARGS[@]}"]="$(platform_path "$ISABELLE_HOME/src/Tools/Setup/isabelle/setup/$SRC")"
-  cp "$ISABELLE_HOME/src/Tools/Setup/isabelle/setup/$SRC" "$SOURCE_DIR"
+  ARGS["${#ARGS[@]}"]="$(platform_path "$ISABELLE_HOME/src/Tools/Setup/src/$SRC")"
+  cp "$ISABELLE_HOME/src/Tools/Setup/src/$SRC" "$SOURCE_DIR"
   echo >> "$BUILD_PROPS" " \\"
   echo -n >> "$BUILD_PROPS" "  src/$SRC"
 done
--- a/src/Tools/Setup/isabelle/setup/Build.java	Sat Jul 17 21:31:15 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,568 +0,0 @@
-/*  Title:      Tools/Setup/isabelle/setup/Build.java
-    Author:     Makarius
-
-Build Isabelle/Scala/Java modules.
-*/
-
-package isabelle.setup;
-
-
-import java.io.BufferedOutputStream;
-import java.io.ByteArrayInputStream;
-import java.io.ByteArrayOutputStream;
-import java.io.CharArrayWriter;
-import java.io.File;
-import java.io.IOException;
-import java.io.InputStream;
-import java.io.PrintStream;
-import java.math.BigInteger;
-import java.nio.charset.StandardCharsets;
-import java.nio.file.Files;
-import java.nio.file.Path;
-import java.nio.file.StandardCopyOption;
-import java.security.MessageDigest;
-import java.security.NoSuchAlgorithmException;
-import java.util.ArrayList;
-import java.util.Comparator;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Locale;
-import java.util.Properties;
-import java.util.TreeMap;
-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;
-
-import javax.tools.JavaCompiler;
-import javax.tools.JavaFileObject;
-import javax.tools.StandardJavaFileManager;
-import javax.tools.ToolProvider;
-
-import scala.tools.nsc.MainClass;
-
-
-public class Build
-{
-    /** context **/
-
-    public static String BUILD_PROPS = "build.props";
-    public static String COMPONENT_BUILD_PROPS = "etc/build.props";
-
-    public static Context directory_context(Path dir)
-        throws IOException
-    {
-        Properties props = new Properties();
-        Path props_path = dir.resolve(BUILD_PROPS);
-        props.load(Files.newBufferedReader(props_path));
-        return new Context(dir, props, props_path.toString());
-    }
-
-    public static Context component_context(Path dir)
-        throws IOException
-    {
-        Properties props = new Properties();
-        Path props_path = dir.resolve(COMPONENT_BUILD_PROPS);
-        if (Files.exists(props_path)) { props.load(Files.newBufferedReader(props_path)); }
-        return new Context(dir, props, props_path.toString());
-    }
-
-    public static List<Context> component_contexts()
-        throws IOException, InterruptedException
-    {
-        List<Context> result = new LinkedList<Context>();
-        for (String p : Environment.getenv("ISABELLE_COMPONENTS").split(":", -1)) {
-            if (!p.isEmpty()) {
-                Path dir = Path.of(Environment.platform_path(p));
-                if (Files.exists(dir.resolve(COMPONENT_BUILD_PROPS))) {
-                    result.add(component_context(dir));
-                }
-            }
-        }
-        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;
-        private final Properties _props;
-        private final String _location;
-
-        public Context(Path dir, Properties props, String location)
-        {
-            _dir = dir;
-            _props = props;
-            _location = location;
-        }
-
-        @Override public String toString() { return _dir.toString(); }
-
-        public String error_message(String msg)
-        {
-            if (_location == null || _location.isEmpty()) {
-                return msg;
-            }
-            else {
-                return msg +" (in " + Library.quote(_location) + ")";
-            }
-        }
-
-        public String title() {
-            String title = _props.getProperty("title", "");
-            if (title.isEmpty()) { throw new RuntimeException(error_message("Missing title")); }
-            else return title;
-        }
-
-        public String no_module() { return _props.getProperty("no_module", ""); }
-        public String module() { return _props.getProperty("module", ""); }
-        public String module_name() {
-            if (!module().isEmpty() && !no_module().isEmpty()) {
-              throw new RuntimeException(error_message("Conflict of module and no_module"));
-            }
-            if (!module().isEmpty()) { return module(); }
-            else { return no_module(); }
-        }
-        public String scalac_options() { return _props.getProperty("scalac_options", ""); }
-        public String javac_options() { return _props.getProperty("javac_options", ""); }
-        public String main() { return _props.getProperty("main", ""); }
-
-        private List<String> get_list(String name)
-        {
-            List<String> list = new LinkedList<String>();
-            for (String s : _props.getProperty(name, "").split("\\s+")) {
-                if (!s.isEmpty()) { list.add(s); }
-            }
-            return List.copyOf(list);
-        }
-        public List<String> requirements() { return get_list("requirements"); }
-        public List<String> sources() { return get_list("sources"); }
-        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
-        {
-            return _dir.resolve(Environment.expand_platform_path(file));
-        }
-        public boolean exists(String file)
-            throws IOException, InterruptedException
-        {
-            return Files.exists(path(file));
-        }
-
-        public List<Path> requirement_paths(String s)
-            throws IOException, InterruptedException
-        {
-            if (s.startsWith("env:")) {
-                List<Path> paths = new LinkedList<Path>();
-                for (String p : Environment.getenv(s.substring(4)).split(":", -1)) {
-                    if (!p.isEmpty()) {
-                        Path path = Path.of(Environment.platform_path(p));
-                        paths.add(path);
-                    }
-                }
-                return List.copyOf(paths);
-            }
-            else { return List.of(path(s)); }
-        }
-
-        public String item_name(String s)
-        {
-            int i = s.indexOf(':');
-            return i > 0 ? s.substring(0, i) : s;
-        }
-
-        public String item_target(String s)
-        {
-            int i = s.indexOf(':');
-            return i > 0 ? s.substring(i + 1) : s;
-        }
-
-        public String shasum(String name, List<Path> paths)
-            throws IOException, NoSuchAlgorithmException
-        {
-            MessageDigest sha = MessageDigest.getInstance("SHA");
-            for (Path file : paths) {
-                if (Files.exists(file)) {
-                    sha.update(Files.readAllBytes(file));
-                }
-                else {
-                    throw new RuntimeException(
-                        error_message("Missing input file " + Library.quote(file.toString())));
-                }
-            }
-            return sha_digest(sha, name);
-        }
-
-        public String shasum(String file)
-            throws IOException, NoSuchAlgorithmException, InterruptedException
-        {
-            return shasum(file, List.of(path(file)));
-        }
-
-        public String shasum_props()
-            throws NoSuchAlgorithmException
-        {
-            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>");
-        }
-    }
-
-
-    /** compile sources **/
-
-    private static void add_options(List<String> options_list, String options)
-    {
-        if (options != null) {
-            for (String s : options.split("\\s+")) {
-                if (!s.isEmpty()) { options_list.add(s); }
-            }
-        }
-    }
-
-    private static void compiler_result(boolean ok, String out, String what)
-    {
-        if (ok) { if (!out.isEmpty()) { System.err.println(out); } }
-        else {
-            String msg = "Failed to compile " + what + (out.isEmpty() ? "" : ":\n" + out);
-            throw new RuntimeException(msg);
-        }
-    }
-
-    public static void compile_scala_sources(
-        Path target_dir, String more_options, List<Path> deps, List<Path> sources)
-        throws IOException, InterruptedException
-    {
-        ArrayList<String> args = new ArrayList<String>();
-        add_options(args, Environment.getenv("ISABELLE_SCALAC_OPTIONS"));
-        add_options(args, more_options);
-        args.add("-d");
-        args.add(target_dir.toString());
-        args.add("-bootclasspath");
-        args.add(Environment.join_platform_paths(deps));
-        args.add("--");
-
-        boolean scala_sources = false;
-        for (Path p : sources) {
-            args.add(p.toString());
-            if (p.toString().endsWith(".scala")) { scala_sources = true; }
-        }
-        if (scala_sources) {
-            InputStream in_orig = System.in;
-            PrintStream out_orig = System.out;
-            PrintStream err_orig = System.err;
-            ByteArrayInputStream in = new ByteArrayInputStream(new byte[0]);
-            ByteArrayOutputStream out = new ByteArrayOutputStream();
-
-            // Single-threaded context!
-            boolean ok = false;
-            try {
-                PrintStream out_stream = new PrintStream(out);
-                System.setIn(in);
-                System.setOut(out_stream);
-                System.setErr(out_stream);
-                ok = new MainClass().process(args.toArray(String[]::new));
-                out_stream.flush();
-            }
-            finally {
-                System.setIn(in_orig);
-                System.setOut(out_orig);
-                System.setErr(err_orig);
-            }
-            compiler_result(ok, out.toString(StandardCharsets.UTF_8), "Scala sources");
-        }
-    }
-
-    public static void compile_java_sources(
-        Path target_dir, String more_options, List<Path> deps, List<Path> sources)
-        throws IOException, InterruptedException
-    {
-        JavaCompiler compiler = ToolProvider.getSystemJavaCompiler();
-        StandardJavaFileManager file_manager =
-            compiler.getStandardFileManager(null, Locale.ROOT, StandardCharsets.UTF_8);
-
-        List<String> options = new LinkedList<String>();
-        add_options(options, Environment.getenv("ISABELLE_JAVAC_OPTIONS"));
-        add_options(options, more_options);
-        options.add("-d");
-        options.add(target_dir.toString());
-        options.add("-classpath");
-        options.add(Environment.join_platform_paths(deps));
-
-        List<JavaFileObject> java_sources = new LinkedList<JavaFileObject>();
-        for (Path p : sources) {
-            if (p.toString().endsWith(".java")) {
-                for (JavaFileObject o : file_manager.getJavaFileObjectsFromPaths(List.of(p))) {
-                    java_sources.add(o);
-                }
-            }
-        }
-
-        if (!java_sources.isEmpty()) {
-            CharArrayWriter out = new CharArrayWriter();
-            boolean ok = compiler.getTask(out, file_manager, null, options, null, java_sources).call();
-            out.flush();
-            compiler_result(ok, out.toString(), "Java sources");
-        }
-    }
-
-
-    /** shasum for jar content **/
-
-    private static String SHASUM = "META-INF/isabelle/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(path.getParent());
-        Files.writeString(path, shasum);
-    }
-
-
-    /** 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)
-        throws IOException
-    {
-        Files.createDirectories(dir.resolve(jar).getParent());
-        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());
-                    if (!name.isEmpty()) {
-                        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();
-                    }
-                }
-            }
-        }
-    }
-
-
-    /** classpath **/
-
-    public static List<Path> classpath()
-        throws IOException, InterruptedException
-    {
-        List<Path> result = new LinkedList<Path>();
-        for (Context context : component_contexts()) {
-            String module = context.module();
-            if (!module.isEmpty()) { result.add(context.path(module)); }
-        }
-        return List.copyOf(result);
-    }
-
-    public static List<String> services()
-        throws IOException, InterruptedException
-    {
-        List<String> result = new LinkedList<String>();
-        for (Context context : component_contexts()) {
-            for (String s : context.services()) {
-                result.add(s);
-            }
-        }
-        return List.copyOf(result);
-    }
-
-
-    /** build **/
-
-    public static void build(Context context, boolean fresh)
-        throws IOException, InterruptedException, NoSuchAlgorithmException
-    {
-        String module = context.module();
-        if (!module.isEmpty()) {
-            String title = context.title();
-
-            Path jar_path = context.path(module);
-            String jar_name = jar_path.toString();
-            if (!jar_name.endsWith(".jar")) {
-                throw new RuntimeException(
-                    context.error_message("Bad jar module " + Library.quote(jar_name)));
-            }
-
-            if (context.is_vacuous()) { Files.deleteIfExists(jar_path); }
-            else {
-                List<String> requirements = context.requirements();
-                List<String> resources = context.resources();
-                List<String> sources = context.sources();
-
-                String shasum_old = get_shasum(jar_path);
-                String shasum;
-                List<Path> compiler_deps = new LinkedList<Path>();
-                {
-                    StringBuilder _shasum = new StringBuilder();
-                    _shasum.append(context.shasum_props());
-                    for (String s : requirements) {
-                        List<Path> paths = context.requirement_paths(s);
-                        compiler_deps.addAll(paths);
-                        _shasum.append(context.shasum(s, paths));
-                    }
-                    for (String s : resources) {
-                        _shasum.append(context.shasum(context.item_name(s)));
-                    }
-                    for (String s : sources) { _shasum.append(context.shasum(s)); }
-                    shasum = _shasum.toString();
-                }
-                if (fresh || !shasum_old.equals(shasum)) {
-                    System.out.print("### Building " + title + " (" + jar_path + ") ...\n");
-
-                    String isabelle_classpath = Environment.getenv("ISABELLE_CLASSPATH");
-
-                    Path build_dir = Files.createTempDirectory("isabelle");
-                    try {
-                        /* compile sources */
-
-                        for (String s : isabelle_classpath.split(":", -1)) {
-                            if (!s.isEmpty()) {
-                              compiler_deps.add(Path.of(Environment.platform_path(s)));
-                            }
-                        }
-
-                        List<Path> compiler_sources = new LinkedList<Path>();
-                        for (String s : sources) { compiler_sources.add(context.path(s)); }
-
-                        compile_scala_sources(
-                            build_dir, context.scalac_options(), compiler_deps, compiler_sources);
-
-                        compiler_deps.add(build_dir);
-                        compile_java_sources(
-                            build_dir, context.javac_options(), compiler_deps, compiler_sources);
-
-
-                        /* copy resources */
-
-                        for (String s : context.resources()) {
-                            String name = context.item_name(s);
-                            String target = context.item_target(s);
-                            Path file_name = Path.of(name).normalize().getFileName();
-                            Path target_path = Path.of(target).normalize();
-
-                            Path target_dir;
-                            Path target_file;
-                            {
-                                if (target.endsWith("/") || target.endsWith("/.")) {
-                                    target_dir = build_dir.resolve(target_path);
-                                    target_file = target_dir.resolve(file_name);
-                                }
-                                else {
-                                    target_file = build_dir.resolve(target_path);
-                                    target_dir = target_file.getParent();
-                                }
-                            }
-                            Files.createDirectories(target_dir);
-                            Files.copy(context.path(name), target_file,
-                                StandardCopyOption.COPY_ATTRIBUTES);
-                        }
-
-
-                        /* packaging */
-
-                        create_shasum(build_dir, shasum);
-                        create_services(build_dir, context.services());
-                        create_jar(build_dir, context.main(), jar_path);
-                    }
-                    finally {
-                        try (Stream<Path> walk = Files.walk(build_dir)) {
-                            walk.sorted(Comparator.reverseOrder())
-                                .map(Path::toFile)
-                                .forEach(File::delete);
-                        }
-                    }
-                }
-            }
-        }
-    }
-
-    public static void build_components(boolean fresh)
-        throws IOException, InterruptedException, NoSuchAlgorithmException
-    {
-        for (Context context : component_contexts()) {
-            build(context, fresh);
-        }
-    }
-}
--- a/src/Tools/Setup/isabelle/setup/Environment.java	Sat Jul 17 21:31:15 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,453 +0,0 @@
-/*  Title:      Tools/Setup/isabelle/setup/Environment.scala
-    Author:     Makarius
-
-Fundamental Isabelle system environment: quasi-static module with
-optional init operation.
-*/
-
-package isabelle.setup;
-
-import java.io.File;
-import java.io.IOException;
-import java.nio.file.Files;
-import java.nio.file.Path;
-import java.util.HashMap;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Locale;
-import java.util.Map;
-import java.util.function.BiFunction;
-import java.util.regex.Matcher;
-import java.util.regex.Pattern;
-
-
-public class Environment
-{
-    /** Support for Cygwin as POSIX emulation on Windows **/
-
-    public static Boolean is_windows()
-    {
-        return System.getProperty("os.name", "").startsWith("Windows");
-    }
-
-
-
-    /* system path representations */
-
-    public static String slashes(String s) { return s.replace('\\', '/'); }
-
-    public static String standard_path(String cygwin_root, String platform_path)
-    {
-        if (is_windows()) {
-            String backslashes = platform_path.replace('/', '\\');
-
-            Pattern root_pattern =
-                Pattern.compile("(?i)" + Pattern.quote(cygwin_root) + "(?:\\\\+|\\z)(.*)");
-            Matcher root_matcher = root_pattern.matcher(backslashes);
-
-            Pattern drive_pattern = Pattern.compile("([a-zA-Z]):\\\\*(.*)");
-            Matcher drive_matcher = drive_pattern.matcher(backslashes);
-
-            if (root_matcher.matches()) {
-                String rest = root_matcher.group(1);
-                return "/" + slashes(rest);
-            }
-            else if (drive_matcher.matches()) {
-                String letter = drive_matcher.group(1).toLowerCase(Locale.ROOT);
-                String rest = drive_matcher.group(2);
-                return "/cygdrive/" + letter + (rest.isEmpty() ? "" : "/" + slashes(rest));
-            }
-            else { return slashes(backslashes); }
-        }
-        else { return platform_path; }
-    }
-
-    private static class Expand_Platform_Path
-    {
-        private String _cygwin_root;
-        private StringBuilder _result = new StringBuilder();
-
-        public Expand_Platform_Path(String cygwin_root)
-        {
-            _cygwin_root = cygwin_root;
-        }
-
-        public String result() { return _result.toString(); }
-
-        void clear() { _result.setLength(0); }
-        void add(char c) { _result.append(c); }
-        void add(String s) { _result.append(s); }
-        void separator()
-        {
-            int n = _result.length();
-            if (n > 0 && _result.charAt(n - 1) != File.separatorChar) {
-                add(File.separatorChar);
-            }
-        }
-
-        public String check_root(String standard_path)
-        {
-            String rest = standard_path;
-            boolean is_root = standard_path.startsWith("/");
-
-            if (is_windows()) {
-                Pattern cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)");
-                Matcher cygdrive_matcher = cygdrive_pattern.matcher(standard_path);
-
-                Pattern named_root_pattern = Pattern.compile("//+([^/]*)(.*)");
-                Matcher named_root_matcher = named_root_pattern.matcher(standard_path);
-
-                if (cygdrive_matcher.matches()) {
-                    String drive = cygdrive_matcher.group(1).toUpperCase(Locale.ROOT);
-                    rest = cygdrive_matcher.group(2);
-                    clear();
-                    add(drive);
-                    add(':');
-                    add(File.separatorChar);
-                }
-                else if (named_root_matcher.matches()) {
-                    String root = named_root_matcher.group(1);
-                    rest = named_root_matcher.group(2);
-                    clear();
-                    add(File.separatorChar);
-                    add(File.separatorChar);
-                    add(root);
-                }
-                else if (is_root) {
-                    clear();
-                    add(_cygwin_root);
-                }
-            }
-            else if (is_root) {
-                clear();
-                add(File.separatorChar);
-            }
-            return rest;
-        }
-
-        public void check_rest(Map<String,String> env, String main)
-            throws IOException, InterruptedException
-        {
-            for (String p : main.split("/", -1)) {
-                if (env != null && p.startsWith("$")) {
-                    String var = p.substring(1);
-                    String res = env.getOrDefault(var, "");
-                    if (res.isEmpty()) {
-                        throw new RuntimeException(
-                            "Bad Isabelle environment variable: " + Library.quote(var));
-                    }
-                    else check(null, res);
-                }
-                else if (!p.isEmpty()) {
-                    separator();
-                    add(p);
-                }
-            }
-        }
-
-        public void check(Map<String,String> env, String path)
-            throws IOException, InterruptedException
-        {
-            check_rest(env, check_root(path));
-        }
-    }
-
-    public static String expand_platform_path(
-        Map<String,String> env, String cygwin_root, String standard_path)
-        throws IOException, InterruptedException
-    {
-        Expand_Platform_Path expand = new Expand_Platform_Path(cygwin_root);
-        expand.check(env, standard_path);
-        return expand.result();
-    }
-
-    public static String join_platform_paths(List<Path> paths)
-    {
-        List<String> strs = new LinkedList<String>();
-        for (Path p : paths) { strs.add(p.toString()); }
-        return String.join(File.pathSeparator, strs);
-    }
-
-    public static String join_standard_paths(List<Path> paths)
-        throws IOException, InterruptedException
-    {
-        List<String> strs = new LinkedList<String>();
-        for (Path p : paths) { strs.add(standard_path(p.toString())); }
-        return String.join(":", strs);
-    }
-
-
-    /* raw process */
-
-    public static ProcessBuilder process_builder(
-        List<String> cmd, File cwd, Map<String,String> env, boolean redirect)
-    {
-        ProcessBuilder builder = new ProcessBuilder();
-
-        // fragile on Windows:
-        // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
-        builder.command(cmd);
-
-        if (cwd != null) builder.directory(cwd);
-        if (env != null) {
-            builder.environment().clear();
-            builder.environment().putAll(env);
-        }
-        builder.redirectErrorStream(redirect);
-
-        return builder;
-    }
-
-    public static class Exec_Result
-    {
-        private final int _rc;
-        private final String _out;
-        private final String _err;
-
-        Exec_Result(int rc, String out, String err)
-        {
-            _rc = rc;
-            _out = Library.trim_line(out);
-            _err = Library.trim_line(err);
-        }
-
-        public int rc() { return _rc; }
-        public boolean ok() { return _rc == 0; }
-        public String out() { return _out; }
-        public String err() { return _err; }
-    }
-
-    public static Exec_Result exec_process(
-        List<String> command_line,
-        File cwd,
-        Map<String,String> env,
-        boolean redirect) throws IOException, InterruptedException
-    {
-        Path out_file = Files.createTempFile(null, null);
-        Path err_file = Files.createTempFile(null, null);
-        Exec_Result res;
-        try {
-            ProcessBuilder builder = process_builder(command_line, cwd, env, redirect);
-            builder.redirectOutput(out_file.toFile());
-            builder.redirectError(err_file.toFile());
-
-            Process proc = builder.start();
-            proc.getOutputStream().close();
-            try { proc.waitFor(); }
-            finally {
-                proc.getInputStream().close();
-                proc.getErrorStream().close();
-                proc.destroy();
-                Thread.interrupted();
-            }
-
-            int rc = proc.exitValue();
-            String out = Files.readString(out_file);
-            String err = Files.readString(err_file);
-            res = new Exec_Result(rc, out, err);
-        }
-        finally {
-            Files.deleteIfExists(out_file);
-            Files.deleteIfExists(err_file);
-        }
-        return res;
-    }
-
-
-    /* init (e.g. after extraction via 7zip) */
-
-    private static String bootstrap_directory(
-        String preference, String variable, String property, String description)
-    {
-        String a = preference;  // explicit argument
-        String b = System.getenv(variable);  // e.g. inherited from running isabelle tool
-        String c = System.getProperty(property);  // e.g. via JVM application boot process
-        String dir;
-
-        if (a != null && !a.isEmpty()) { dir = a; }
-        else if (b != null && !b.isEmpty()) { dir = b; }
-        else if (c != null && !c.isEmpty()) { dir = c; }
-        else { throw new RuntimeException("Unknown " + description + " directory"); }
-
-        if ((new File(dir)).isDirectory()) { return dir; }
-        else {
-            throw new RuntimeException("Bad " + description + " directory " + Library.quote(dir));
-        }
-    }
-
-    private static void cygwin_exec(String isabelle_root, List<String> cmd)
-        throws IOException, InterruptedException
-    {
-        File cwd = new File(isabelle_root);
-        Map<String,String> env = new HashMap<String,String>(System.getenv());
-        env.put("CYGWIN", "nodosfilewarning");
-        Exec_Result res = exec_process(cmd, cwd, env, true);
-        if (!res.ok()) throw new RuntimeException(res.out());
-    }
-
-    public static void cygwin_link(String content, File target) throws IOException
-    {
-        Path target_path = target.toPath();
-        Files.writeString(target_path, "!<symlink>" + content + "\u0000");
-        Files.setAttribute(target_path, "dos:system", true);
-    }
-
-    public static void cygwin_init(String isabelle_root, String cygwin_root)
-        throws IOException, InterruptedException
-    {
-        if (is_windows()) {
-            File uninitialized_file = new File(cygwin_root, "isabelle\\uninitialized");
-            boolean uninitialized = uninitialized_file.isFile() && uninitialized_file.delete();
-
-            if (uninitialized) {
-                Path symlinks_path = (new File(cygwin_root + "\\isabelle\\symlinks")).toPath();
-                String[] symlinks = Files.readAllLines(symlinks_path).toArray(new String[0]);
-
-                // recover symlinks
-                int i = 0;
-                int m = symlinks.length;
-                int n = (m > 0 && symlinks[m - 1].isEmpty()) ? m - 1 : m;
-                while (i < n) {
-                    if (i + 1 < n) {
-                        String target = symlinks[i];
-                        String content = symlinks[i + 1];
-                        cygwin_link(content, new File(isabelle_root, target));
-                        i += 2;
-                    } else { throw new RuntimeException("Unbalanced symlinks list"); }
-                }
-
-                cygwin_exec(isabelle_root,
-                    List.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall"));
-                cygwin_exec(isabelle_root,
-                    List.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall"));
-            }
-        }
-    }
-
-
-    /* implicit settings environment */
-
-    private static volatile Map<String,String> _settings = null;
-
-    public static Map<String,String> settings()
-        throws IOException, InterruptedException
-    {
-        if (_settings == null) { init("", ""); }  // unsynchronized check
-        return _settings;
-    }
-
-    public static String getenv(String name)
-        throws IOException, InterruptedException
-    {
-        return settings().getOrDefault(name, "");
-    }
-
-    public static synchronized void init(String _isabelle_root, String _cygwin_root)
-        throws IOException, InterruptedException
-    {
-        if (_settings == null) {
-            String isabelle_root =
-                bootstrap_directory(_isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root");
-
-            String cygwin_root = "";
-            if (is_windows()) {
-                cygwin_root = bootstrap_directory(_cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root");
-                cygwin_init(isabelle_root, cygwin_root);
-            }
-
-            Map<String,String> env = new HashMap<String,String>(System.getenv());
-
-            BiFunction<String,String,Void> env_default =
-                (String a, String b) -> { if (!b.isEmpty()) env.putIfAbsent(a, b); return null; };
-
-            String temp_windows = is_windows() ? System.getenv("TEMP") : null;
-
-            env_default.apply("CYGWIN_ROOT", cygwin_root);
-            env_default.apply("TEMP_WINDOWS",
-                (temp_windows != null && temp_windows.contains("\\")) ? temp_windows : "");
-            env_default.apply("ISABELLE_JDK_HOME",
-                standard_path(cygwin_root, System.getProperty("java.home", "")));
-            env_default.apply("HOME", System.getProperty("user.home", ""));
-            env_default.apply("ISABELLE_APP", System.getProperty("isabelle.app", ""));
-
-            Map<String,String> settings = new HashMap<String,String>();
-            Path settings_file = Files.createTempFile(null, null);
-            try {
-                List<String> cmd = new LinkedList<String>();
-                if (is_windows()) {
-                    cmd.add(cygwin_root + "\\bin\\bash");
-                    cmd.add("-l");
-                    cmd.add(standard_path(cygwin_root, isabelle_root + "\\bin\\isabelle"));
-                } else {
-                    cmd.add(isabelle_root + "/bin/isabelle");
-                }
-                cmd.add("getenv");
-                cmd.add("-d");
-                cmd.add(settings_file.toString());
-
-                Exec_Result res = exec_process(cmd, null, env, true);
-                if (!res.ok()) throw new RuntimeException(res.out());
-
-                for (String s : Files.readString(settings_file).split("\u0000", -1)) {
-                    int i = s.indexOf('=');
-                    if (i > 0) { settings.put(s.substring(0, i), s.substring(i + 1)); }
-                    else if (i < 0 && !s.isEmpty()) { settings.put(s, ""); }
-                }
-            }
-            finally { Files.delete(settings_file); }
-
-            if (is_windows()) { settings.put("CYGWIN_ROOT", cygwin_root); }
-
-            settings.put("PATH", settings.get("PATH_JVM"));
-            settings.remove("PATH_JVM");
-
-            _settings = Map.copyOf(settings);
-        }
-    }
-
-
-    /* Cygwin root (after init) */
-
-    public static String cygwin_root()
-        throws IOException, InterruptedException
-    {
-        return getenv("CYGWIN_ROOT");
-    }
-
-    public static String standard_path(String platform_path)
-        throws IOException, InterruptedException
-    {
-        return standard_path(cygwin_root(), platform_path);
-    }
-
-    public static String expand_platform_path(String standard_path)
-            throws IOException, InterruptedException
-    {
-        return expand_platform_path(settings(), cygwin_root(), standard_path);
-    }
-
-    public static String platform_path(String standard_path)
-        throws IOException, InterruptedException
-    {
-        return expand_platform_path(null, cygwin_root(), standard_path);
-    }
-
-
-    /* kill process (via bash) */
-
-    static public boolean kill_process(String group_pid, String signal)
-        throws IOException, InterruptedException
-    {
-        List<String> cmd = new LinkedList<String>();
-        if (is_windows()) {
-            cmd.add(cygwin_root() + "\\bin\\bash.exe");
-        }
-        else {
-            cmd.add("/usr/bin/env");
-            cmd.add("bash");
-        }
-        cmd.add("-c");
-        cmd.add("kill -" + signal + " -" + group_pid);
-        return exec_process(cmd, null, null, false).ok();
-    }
-}
--- a/src/Tools/Setup/isabelle/setup/Exn.java	Sat Jul 17 21:31:15 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-/*  Title:      Tools/Setup/isabelle/setup/Exn.java
-    Author:     Makarius
-
-Support for exceptions (arbitrary throwables).
-*/
-
-package isabelle.setup;
-
-
-import java.io.IOException;
-import java.util.LinkedList;
-import java.util.List;
-
-
-public class Exn
-{
-    /* interrupts */
-
-    public static boolean is_interrupt(Throwable exn)
-    {
-        boolean found_interrupt = false;
-        Throwable e = exn;
-        while (!found_interrupt && e != null) {
-            found_interrupt = e instanceof InterruptedException;
-            e = e.getCause();
-        }
-        return found_interrupt;
-    }
-
-    public static int INTERRUPT_RETURN_CODE = 130;
-
-    public static int return_code(Throwable exn, int rc)
-    {
-        return is_interrupt(exn) ? INTERRUPT_RETURN_CODE : rc;
-    }
-
-
-    /* message */
-
-    public static String message(Throwable exn)
-    {
-        String msg = exn.getMessage();
-
-        if (exn.getClass() == RuntimeException.class)
-        {
-            return msg == null || msg.isEmpty() ? "Error" : msg;
-        }
-        else if (exn instanceof IOException)
-        {
-            return msg == null || msg.isEmpty() ? "I/O error" : "I/O error: " + msg;
-        }
-        else if (exn instanceof RuntimeException && !msg.isEmpty()) { return msg; }
-        else if (exn instanceof InterruptedException) { return "Interrupt"; }
-        else { return exn.toString(); }
-    }
-
-
-    /* print */
-
-    public static String trace(Throwable exn)
-    {
-        List<String> list = new LinkedList<String>();
-        for (StackTraceElement elem : exn.getStackTrace()) {
-            list.add(elem.toString());
-        }
-        return Library.cat_lines(list);
-    }
-
-    public static boolean debug()
-    {
-        return System.getProperty("isabelle.debug", "").equals("true");
-    }
-
-    public static String print(Throwable exn)
-    {
-        return debug() ? message(exn) + "\n" + trace(exn) : message(exn);
-    }
-
-    public static String print_error(Throwable exn)
-    {
-        return Library.prefix_lines("*** ", print(exn));
-    }
-}
--- a/src/Tools/Setup/isabelle/setup/Library.java	Sat Jul 17 21:31:15 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-/*  Title:      Tools/Setup/isabelle/setup/Library.java
-    Author:     Makarius
-
-Basic library.
-*/
-
-package isabelle.setup;
-
-
-import java.util.Arrays;
-import java.util.LinkedList;
-import java.util.List;
-
-
-public class Library
-{
-    public static String quote(String s)
-    {
-        return "\"" + s + "\"";
-    }
-
-    public static String cat_lines(Iterable<? extends CharSequence> lines)
-    {
-        return String.join("\n", lines);
-    }
-
-    public static List<String> split_lines(String str)
-    {
-        if (str.isEmpty()) { return List.of(); }
-        else {
-            List<String> result = new LinkedList<String>();
-            result.addAll(Arrays.asList(str.split("\\n")));
-            return List.copyOf(result);
-        }
-    }
-
-    public static String prefix_lines(String prfx, String str)
-    {
-        if (str.isEmpty()) { return str; }
-        else {
-            List<String> lines = new LinkedList<String>();
-            for (String line : split_lines(str)) { lines.add(prfx + line); }
-            return cat_lines(lines);
-        }
-    }
-
-    public static String trim_line(String s)
-    {
-        if (s.endsWith("\r\n")) { return s.substring(0, s.length() - 2); }
-        else if (s.endsWith("\r") || s.endsWith("\n")) { return s.substring(0, s.length() - 1); }
-        else { return s; }
-    }
-}
\ No newline at end of file
--- a/src/Tools/Setup/isabelle/setup/Setup.java	Sat Jul 17 21:31:15 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-/*  Title:      Tools/Setup/isabelle/setup/Setup.java
-    Author:     Makarius
-
-Isabelle setup tool: bootstrap from generic Java environment.
-*/
-
-package isabelle.setup;
-
-
-class Setup
-{
-    private static void echo(String msg)
-    {
-        System.out.print(msg + "\n");
-    }
-    private static void echo_err(String msg)
-    {
-        System.err.print(msg + "\n");
-    }
-    private static void fail(String msg)
-    {
-        echo_err(msg);
-        System.exit(2);
-    }
-
-    private static void check_args(boolean b)
-    {
-        if (!b) { fail("Bad command-line arguments"); }
-    }
-
-    public static void main(String[] args)
-    {
-        int n = args.length;
-        check_args(n > 0);
-
-        String op = args[0];
-        try {
-            switch (op) {
-                case "build":
-                    check_args(n == 1);
-                    Build.build_components(false);
-                    break;
-                case "build_fresh":
-                    check_args(n == 1);
-                    Build.build_components(true);
-                    break;
-                case "classpath":
-                    check_args(n == 1);
-                    echo(Environment.join_standard_paths(Build.classpath()));
-                    break;
-                case "services":
-                    check_args(n == 1);
-                    for (String s : Build.services()) { echo(s); }
-                    break;
-                default:
-                    fail("Bad setup operation " + Library.quote(op));
-                    break;
-            }
-        }
-        catch (Throwable exn) {
-            echo_err(Exn.print_error(exn));
-            System.exit(Exn.return_code(exn, 2));
-        }
-    }
-}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/src/Build.java	Sat Jul 17 21:40:57 2021 +0200
@@ -0,0 +1,568 @@
+/*  Title:      Tools/Setup/src/Build.java
+    Author:     Makarius
+
+Build Isabelle/Scala/Java modules.
+*/
+
+package isabelle.setup;
+
+
+import java.io.BufferedOutputStream;
+import java.io.ByteArrayInputStream;
+import java.io.ByteArrayOutputStream;
+import java.io.CharArrayWriter;
+import java.io.File;
+import java.io.IOException;
+import java.io.InputStream;
+import java.io.PrintStream;
+import java.math.BigInteger;
+import java.nio.charset.StandardCharsets;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.StandardCopyOption;
+import java.security.MessageDigest;
+import java.security.NoSuchAlgorithmException;
+import java.util.ArrayList;
+import java.util.Comparator;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Locale;
+import java.util.Properties;
+import java.util.TreeMap;
+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;
+
+import javax.tools.JavaCompiler;
+import javax.tools.JavaFileObject;
+import javax.tools.StandardJavaFileManager;
+import javax.tools.ToolProvider;
+
+import scala.tools.nsc.MainClass;
+
+
+public class Build
+{
+    /** context **/
+
+    public static String BUILD_PROPS = "build.props";
+    public static String COMPONENT_BUILD_PROPS = "etc/build.props";
+
+    public static Context directory_context(Path dir)
+        throws IOException
+    {
+        Properties props = new Properties();
+        Path props_path = dir.resolve(BUILD_PROPS);
+        props.load(Files.newBufferedReader(props_path));
+        return new Context(dir, props, props_path.toString());
+    }
+
+    public static Context component_context(Path dir)
+        throws IOException
+    {
+        Properties props = new Properties();
+        Path props_path = dir.resolve(COMPONENT_BUILD_PROPS);
+        if (Files.exists(props_path)) { props.load(Files.newBufferedReader(props_path)); }
+        return new Context(dir, props, props_path.toString());
+    }
+
+    public static List<Context> component_contexts()
+        throws IOException, InterruptedException
+    {
+        List<Context> result = new LinkedList<Context>();
+        for (String p : Environment.getenv("ISABELLE_COMPONENTS").split(":", -1)) {
+            if (!p.isEmpty()) {
+                Path dir = Path.of(Environment.platform_path(p));
+                if (Files.exists(dir.resolve(COMPONENT_BUILD_PROPS))) {
+                    result.add(component_context(dir));
+                }
+            }
+        }
+        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;
+        private final Properties _props;
+        private final String _location;
+
+        public Context(Path dir, Properties props, String location)
+        {
+            _dir = dir;
+            _props = props;
+            _location = location;
+        }
+
+        @Override public String toString() { return _dir.toString(); }
+
+        public String error_message(String msg)
+        {
+            if (_location == null || _location.isEmpty()) {
+                return msg;
+            }
+            else {
+                return msg +" (in " + Library.quote(_location) + ")";
+            }
+        }
+
+        public String title() {
+            String title = _props.getProperty("title", "");
+            if (title.isEmpty()) { throw new RuntimeException(error_message("Missing title")); }
+            else return title;
+        }
+
+        public String no_module() { return _props.getProperty("no_module", ""); }
+        public String module() { return _props.getProperty("module", ""); }
+        public String module_name() {
+            if (!module().isEmpty() && !no_module().isEmpty()) {
+              throw new RuntimeException(error_message("Conflict of module and no_module"));
+            }
+            if (!module().isEmpty()) { return module(); }
+            else { return no_module(); }
+        }
+        public String scalac_options() { return _props.getProperty("scalac_options", ""); }
+        public String javac_options() { return _props.getProperty("javac_options", ""); }
+        public String main() { return _props.getProperty("main", ""); }
+
+        private List<String> get_list(String name)
+        {
+            List<String> list = new LinkedList<String>();
+            for (String s : _props.getProperty(name, "").split("\\s+")) {
+                if (!s.isEmpty()) { list.add(s); }
+            }
+            return List.copyOf(list);
+        }
+        public List<String> requirements() { return get_list("requirements"); }
+        public List<String> sources() { return get_list("sources"); }
+        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
+        {
+            return _dir.resolve(Environment.expand_platform_path(file));
+        }
+        public boolean exists(String file)
+            throws IOException, InterruptedException
+        {
+            return Files.exists(path(file));
+        }
+
+        public List<Path> requirement_paths(String s)
+            throws IOException, InterruptedException
+        {
+            if (s.startsWith("env:")) {
+                List<Path> paths = new LinkedList<Path>();
+                for (String p : Environment.getenv(s.substring(4)).split(":", -1)) {
+                    if (!p.isEmpty()) {
+                        Path path = Path.of(Environment.platform_path(p));
+                        paths.add(path);
+                    }
+                }
+                return List.copyOf(paths);
+            }
+            else { return List.of(path(s)); }
+        }
+
+        public String item_name(String s)
+        {
+            int i = s.indexOf(':');
+            return i > 0 ? s.substring(0, i) : s;
+        }
+
+        public String item_target(String s)
+        {
+            int i = s.indexOf(':');
+            return i > 0 ? s.substring(i + 1) : s;
+        }
+
+        public String shasum(String name, List<Path> paths)
+            throws IOException, NoSuchAlgorithmException
+        {
+            MessageDigest sha = MessageDigest.getInstance("SHA");
+            for (Path file : paths) {
+                if (Files.exists(file)) {
+                    sha.update(Files.readAllBytes(file));
+                }
+                else {
+                    throw new RuntimeException(
+                        error_message("Missing input file " + Library.quote(file.toString())));
+                }
+            }
+            return sha_digest(sha, name);
+        }
+
+        public String shasum(String file)
+            throws IOException, NoSuchAlgorithmException, InterruptedException
+        {
+            return shasum(file, List.of(path(file)));
+        }
+
+        public String shasum_props()
+            throws NoSuchAlgorithmException
+        {
+            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>");
+        }
+    }
+
+
+    /** compile sources **/
+
+    private static void add_options(List<String> options_list, String options)
+    {
+        if (options != null) {
+            for (String s : options.split("\\s+")) {
+                if (!s.isEmpty()) { options_list.add(s); }
+            }
+        }
+    }
+
+    private static void compiler_result(boolean ok, String out, String what)
+    {
+        if (ok) { if (!out.isEmpty()) { System.err.println(out); } }
+        else {
+            String msg = "Failed to compile " + what + (out.isEmpty() ? "" : ":\n" + out);
+            throw new RuntimeException(msg);
+        }
+    }
+
+    public static void compile_scala_sources(
+        Path target_dir, String more_options, List<Path> deps, List<Path> sources)
+        throws IOException, InterruptedException
+    {
+        ArrayList<String> args = new ArrayList<String>();
+        add_options(args, Environment.getenv("ISABELLE_SCALAC_OPTIONS"));
+        add_options(args, more_options);
+        args.add("-d");
+        args.add(target_dir.toString());
+        args.add("-bootclasspath");
+        args.add(Environment.join_platform_paths(deps));
+        args.add("--");
+
+        boolean scala_sources = false;
+        for (Path p : sources) {
+            args.add(p.toString());
+            if (p.toString().endsWith(".scala")) { scala_sources = true; }
+        }
+        if (scala_sources) {
+            InputStream in_orig = System.in;
+            PrintStream out_orig = System.out;
+            PrintStream err_orig = System.err;
+            ByteArrayInputStream in = new ByteArrayInputStream(new byte[0]);
+            ByteArrayOutputStream out = new ByteArrayOutputStream();
+
+            // Single-threaded context!
+            boolean ok = false;
+            try {
+                PrintStream out_stream = new PrintStream(out);
+                System.setIn(in);
+                System.setOut(out_stream);
+                System.setErr(out_stream);
+                ok = new MainClass().process(args.toArray(String[]::new));
+                out_stream.flush();
+            }
+            finally {
+                System.setIn(in_orig);
+                System.setOut(out_orig);
+                System.setErr(err_orig);
+            }
+            compiler_result(ok, out.toString(StandardCharsets.UTF_8), "Scala sources");
+        }
+    }
+
+    public static void compile_java_sources(
+        Path target_dir, String more_options, List<Path> deps, List<Path> sources)
+        throws IOException, InterruptedException
+    {
+        JavaCompiler compiler = ToolProvider.getSystemJavaCompiler();
+        StandardJavaFileManager file_manager =
+            compiler.getStandardFileManager(null, Locale.ROOT, StandardCharsets.UTF_8);
+
+        List<String> options = new LinkedList<String>();
+        add_options(options, Environment.getenv("ISABELLE_JAVAC_OPTIONS"));
+        add_options(options, more_options);
+        options.add("-d");
+        options.add(target_dir.toString());
+        options.add("-classpath");
+        options.add(Environment.join_platform_paths(deps));
+
+        List<JavaFileObject> java_sources = new LinkedList<JavaFileObject>();
+        for (Path p : sources) {
+            if (p.toString().endsWith(".java")) {
+                for (JavaFileObject o : file_manager.getJavaFileObjectsFromPaths(List.of(p))) {
+                    java_sources.add(o);
+                }
+            }
+        }
+
+        if (!java_sources.isEmpty()) {
+            CharArrayWriter out = new CharArrayWriter();
+            boolean ok = compiler.getTask(out, file_manager, null, options, null, java_sources).call();
+            out.flush();
+            compiler_result(ok, out.toString(), "Java sources");
+        }
+    }
+
+
+    /** shasum for jar content **/
+
+    private static String SHASUM = "META-INF/isabelle/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(path.getParent());
+        Files.writeString(path, shasum);
+    }
+
+
+    /** 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)
+        throws IOException
+    {
+        Files.createDirectories(dir.resolve(jar).getParent());
+        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());
+                    if (!name.isEmpty()) {
+                        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();
+                    }
+                }
+            }
+        }
+    }
+
+
+    /** classpath **/
+
+    public static List<Path> classpath()
+        throws IOException, InterruptedException
+    {
+        List<Path> result = new LinkedList<Path>();
+        for (Context context : component_contexts()) {
+            String module = context.module();
+            if (!module.isEmpty()) { result.add(context.path(module)); }
+        }
+        return List.copyOf(result);
+    }
+
+    public static List<String> services()
+        throws IOException, InterruptedException
+    {
+        List<String> result = new LinkedList<String>();
+        for (Context context : component_contexts()) {
+            for (String s : context.services()) {
+                result.add(s);
+            }
+        }
+        return List.copyOf(result);
+    }
+
+
+    /** build **/
+
+    public static void build(Context context, boolean fresh)
+        throws IOException, InterruptedException, NoSuchAlgorithmException
+    {
+        String module = context.module();
+        if (!module.isEmpty()) {
+            String title = context.title();
+
+            Path jar_path = context.path(module);
+            String jar_name = jar_path.toString();
+            if (!jar_name.endsWith(".jar")) {
+                throw new RuntimeException(
+                    context.error_message("Bad jar module " + Library.quote(jar_name)));
+            }
+
+            if (context.is_vacuous()) { Files.deleteIfExists(jar_path); }
+            else {
+                List<String> requirements = context.requirements();
+                List<String> resources = context.resources();
+                List<String> sources = context.sources();
+
+                String shasum_old = get_shasum(jar_path);
+                String shasum;
+                List<Path> compiler_deps = new LinkedList<Path>();
+                {
+                    StringBuilder _shasum = new StringBuilder();
+                    _shasum.append(context.shasum_props());
+                    for (String s : requirements) {
+                        List<Path> paths = context.requirement_paths(s);
+                        compiler_deps.addAll(paths);
+                        _shasum.append(context.shasum(s, paths));
+                    }
+                    for (String s : resources) {
+                        _shasum.append(context.shasum(context.item_name(s)));
+                    }
+                    for (String s : sources) { _shasum.append(context.shasum(s)); }
+                    shasum = _shasum.toString();
+                }
+                if (fresh || !shasum_old.equals(shasum)) {
+                    System.out.print("### Building " + title + " (" + jar_path + ") ...\n");
+
+                    String isabelle_classpath = Environment.getenv("ISABELLE_CLASSPATH");
+
+                    Path build_dir = Files.createTempDirectory("isabelle");
+                    try {
+                        /* compile sources */
+
+                        for (String s : isabelle_classpath.split(":", -1)) {
+                            if (!s.isEmpty()) {
+                              compiler_deps.add(Path.of(Environment.platform_path(s)));
+                            }
+                        }
+
+                        List<Path> compiler_sources = new LinkedList<Path>();
+                        for (String s : sources) { compiler_sources.add(context.path(s)); }
+
+                        compile_scala_sources(
+                            build_dir, context.scalac_options(), compiler_deps, compiler_sources);
+
+                        compiler_deps.add(build_dir);
+                        compile_java_sources(
+                            build_dir, context.javac_options(), compiler_deps, compiler_sources);
+
+
+                        /* copy resources */
+
+                        for (String s : context.resources()) {
+                            String name = context.item_name(s);
+                            String target = context.item_target(s);
+                            Path file_name = Path.of(name).normalize().getFileName();
+                            Path target_path = Path.of(target).normalize();
+
+                            Path target_dir;
+                            Path target_file;
+                            {
+                                if (target.endsWith("/") || target.endsWith("/.")) {
+                                    target_dir = build_dir.resolve(target_path);
+                                    target_file = target_dir.resolve(file_name);
+                                }
+                                else {
+                                    target_file = build_dir.resolve(target_path);
+                                    target_dir = target_file.getParent();
+                                }
+                            }
+                            Files.createDirectories(target_dir);
+                            Files.copy(context.path(name), target_file,
+                                StandardCopyOption.COPY_ATTRIBUTES);
+                        }
+
+
+                        /* packaging */
+
+                        create_shasum(build_dir, shasum);
+                        create_services(build_dir, context.services());
+                        create_jar(build_dir, context.main(), jar_path);
+                    }
+                    finally {
+                        try (Stream<Path> walk = Files.walk(build_dir)) {
+                            walk.sorted(Comparator.reverseOrder())
+                                .map(Path::toFile)
+                                .forEach(File::delete);
+                        }
+                    }
+                }
+            }
+        }
+    }
+
+    public static void build_components(boolean fresh)
+        throws IOException, InterruptedException, NoSuchAlgorithmException
+    {
+        for (Context context : component_contexts()) {
+            build(context, fresh);
+        }
+    }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/src/Environment.java	Sat Jul 17 21:40:57 2021 +0200
@@ -0,0 +1,453 @@
+/*  Title:      Tools/Setup/src/Environment.scala
+    Author:     Makarius
+
+Fundamental Isabelle system environment: quasi-static module with
+optional init operation.
+*/
+
+package isabelle.setup;
+
+import java.io.File;
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.HashMap;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Locale;
+import java.util.Map;
+import java.util.function.BiFunction;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+
+
+public class Environment
+{
+    /** Support for Cygwin as POSIX emulation on Windows **/
+
+    public static Boolean is_windows()
+    {
+        return System.getProperty("os.name", "").startsWith("Windows");
+    }
+
+
+
+    /* system path representations */
+
+    public static String slashes(String s) { return s.replace('\\', '/'); }
+
+    public static String standard_path(String cygwin_root, String platform_path)
+    {
+        if (is_windows()) {
+            String backslashes = platform_path.replace('/', '\\');
+
+            Pattern root_pattern =
+                Pattern.compile("(?i)" + Pattern.quote(cygwin_root) + "(?:\\\\+|\\z)(.*)");
+            Matcher root_matcher = root_pattern.matcher(backslashes);
+
+            Pattern drive_pattern = Pattern.compile("([a-zA-Z]):\\\\*(.*)");
+            Matcher drive_matcher = drive_pattern.matcher(backslashes);
+
+            if (root_matcher.matches()) {
+                String rest = root_matcher.group(1);
+                return "/" + slashes(rest);
+            }
+            else if (drive_matcher.matches()) {
+                String letter = drive_matcher.group(1).toLowerCase(Locale.ROOT);
+                String rest = drive_matcher.group(2);
+                return "/cygdrive/" + letter + (rest.isEmpty() ? "" : "/" + slashes(rest));
+            }
+            else { return slashes(backslashes); }
+        }
+        else { return platform_path; }
+    }
+
+    private static class Expand_Platform_Path
+    {
+        private String _cygwin_root;
+        private StringBuilder _result = new StringBuilder();
+
+        public Expand_Platform_Path(String cygwin_root)
+        {
+            _cygwin_root = cygwin_root;
+        }
+
+        public String result() { return _result.toString(); }
+
+        void clear() { _result.setLength(0); }
+        void add(char c) { _result.append(c); }
+        void add(String s) { _result.append(s); }
+        void separator()
+        {
+            int n = _result.length();
+            if (n > 0 && _result.charAt(n - 1) != File.separatorChar) {
+                add(File.separatorChar);
+            }
+        }
+
+        public String check_root(String standard_path)
+        {
+            String rest = standard_path;
+            boolean is_root = standard_path.startsWith("/");
+
+            if (is_windows()) {
+                Pattern cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)");
+                Matcher cygdrive_matcher = cygdrive_pattern.matcher(standard_path);
+
+                Pattern named_root_pattern = Pattern.compile("//+([^/]*)(.*)");
+                Matcher named_root_matcher = named_root_pattern.matcher(standard_path);
+
+                if (cygdrive_matcher.matches()) {
+                    String drive = cygdrive_matcher.group(1).toUpperCase(Locale.ROOT);
+                    rest = cygdrive_matcher.group(2);
+                    clear();
+                    add(drive);
+                    add(':');
+                    add(File.separatorChar);
+                }
+                else if (named_root_matcher.matches()) {
+                    String root = named_root_matcher.group(1);
+                    rest = named_root_matcher.group(2);
+                    clear();
+                    add(File.separatorChar);
+                    add(File.separatorChar);
+                    add(root);
+                }
+                else if (is_root) {
+                    clear();
+                    add(_cygwin_root);
+                }
+            }
+            else if (is_root) {
+                clear();
+                add(File.separatorChar);
+            }
+            return rest;
+        }
+
+        public void check_rest(Map<String,String> env, String main)
+            throws IOException, InterruptedException
+        {
+            for (String p : main.split("/", -1)) {
+                if (env != null && p.startsWith("$")) {
+                    String var = p.substring(1);
+                    String res = env.getOrDefault(var, "");
+                    if (res.isEmpty()) {
+                        throw new RuntimeException(
+                            "Bad Isabelle environment variable: " + Library.quote(var));
+                    }
+                    else check(null, res);
+                }
+                else if (!p.isEmpty()) {
+                    separator();
+                    add(p);
+                }
+            }
+        }
+
+        public void check(Map<String,String> env, String path)
+            throws IOException, InterruptedException
+        {
+            check_rest(env, check_root(path));
+        }
+    }
+
+    public static String expand_platform_path(
+        Map<String,String> env, String cygwin_root, String standard_path)
+        throws IOException, InterruptedException
+    {
+        Expand_Platform_Path expand = new Expand_Platform_Path(cygwin_root);
+        expand.check(env, standard_path);
+        return expand.result();
+    }
+
+    public static String join_platform_paths(List<Path> paths)
+    {
+        List<String> strs = new LinkedList<String>();
+        for (Path p : paths) { strs.add(p.toString()); }
+        return String.join(File.pathSeparator, strs);
+    }
+
+    public static String join_standard_paths(List<Path> paths)
+        throws IOException, InterruptedException
+    {
+        List<String> strs = new LinkedList<String>();
+        for (Path p : paths) { strs.add(standard_path(p.toString())); }
+        return String.join(":", strs);
+    }
+
+
+    /* raw process */
+
+    public static ProcessBuilder process_builder(
+        List<String> cmd, File cwd, Map<String,String> env, boolean redirect)
+    {
+        ProcessBuilder builder = new ProcessBuilder();
+
+        // fragile on Windows:
+        // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
+        builder.command(cmd);
+
+        if (cwd != null) builder.directory(cwd);
+        if (env != null) {
+            builder.environment().clear();
+            builder.environment().putAll(env);
+        }
+        builder.redirectErrorStream(redirect);
+
+        return builder;
+    }
+
+    public static class Exec_Result
+    {
+        private final int _rc;
+        private final String _out;
+        private final String _err;
+
+        Exec_Result(int rc, String out, String err)
+        {
+            _rc = rc;
+            _out = Library.trim_line(out);
+            _err = Library.trim_line(err);
+        }
+
+        public int rc() { return _rc; }
+        public boolean ok() { return _rc == 0; }
+        public String out() { return _out; }
+        public String err() { return _err; }
+    }
+
+    public static Exec_Result exec_process(
+        List<String> command_line,
+        File cwd,
+        Map<String,String> env,
+        boolean redirect) throws IOException, InterruptedException
+    {
+        Path out_file = Files.createTempFile(null, null);
+        Path err_file = Files.createTempFile(null, null);
+        Exec_Result res;
+        try {
+            ProcessBuilder builder = process_builder(command_line, cwd, env, redirect);
+            builder.redirectOutput(out_file.toFile());
+            builder.redirectError(err_file.toFile());
+
+            Process proc = builder.start();
+            proc.getOutputStream().close();
+            try { proc.waitFor(); }
+            finally {
+                proc.getInputStream().close();
+                proc.getErrorStream().close();
+                proc.destroy();
+                Thread.interrupted();
+            }
+
+            int rc = proc.exitValue();
+            String out = Files.readString(out_file);
+            String err = Files.readString(err_file);
+            res = new Exec_Result(rc, out, err);
+        }
+        finally {
+            Files.deleteIfExists(out_file);
+            Files.deleteIfExists(err_file);
+        }
+        return res;
+    }
+
+
+    /* init (e.g. after extraction via 7zip) */
+
+    private static String bootstrap_directory(
+        String preference, String variable, String property, String description)
+    {
+        String a = preference;  // explicit argument
+        String b = System.getenv(variable);  // e.g. inherited from running isabelle tool
+        String c = System.getProperty(property);  // e.g. via JVM application boot process
+        String dir;
+
+        if (a != null && !a.isEmpty()) { dir = a; }
+        else if (b != null && !b.isEmpty()) { dir = b; }
+        else if (c != null && !c.isEmpty()) { dir = c; }
+        else { throw new RuntimeException("Unknown " + description + " directory"); }
+
+        if ((new File(dir)).isDirectory()) { return dir; }
+        else {
+            throw new RuntimeException("Bad " + description + " directory " + Library.quote(dir));
+        }
+    }
+
+    private static void cygwin_exec(String isabelle_root, List<String> cmd)
+        throws IOException, InterruptedException
+    {
+        File cwd = new File(isabelle_root);
+        Map<String,String> env = new HashMap<String,String>(System.getenv());
+        env.put("CYGWIN", "nodosfilewarning");
+        Exec_Result res = exec_process(cmd, cwd, env, true);
+        if (!res.ok()) throw new RuntimeException(res.out());
+    }
+
+    public static void cygwin_link(String content, File target) throws IOException
+    {
+        Path target_path = target.toPath();
+        Files.writeString(target_path, "!<symlink>" + content + "\u0000");
+        Files.setAttribute(target_path, "dos:system", true);
+    }
+
+    public static void cygwin_init(String isabelle_root, String cygwin_root)
+        throws IOException, InterruptedException
+    {
+        if (is_windows()) {
+            File uninitialized_file = new File(cygwin_root, "isabelle\\uninitialized");
+            boolean uninitialized = uninitialized_file.isFile() && uninitialized_file.delete();
+
+            if (uninitialized) {
+                Path symlinks_path = (new File(cygwin_root + "\\isabelle\\symlinks")).toPath();
+                String[] symlinks = Files.readAllLines(symlinks_path).toArray(new String[0]);
+
+                // recover symlinks
+                int i = 0;
+                int m = symlinks.length;
+                int n = (m > 0 && symlinks[m - 1].isEmpty()) ? m - 1 : m;
+                while (i < n) {
+                    if (i + 1 < n) {
+                        String target = symlinks[i];
+                        String content = symlinks[i + 1];
+                        cygwin_link(content, new File(isabelle_root, target));
+                        i += 2;
+                    } else { throw new RuntimeException("Unbalanced symlinks list"); }
+                }
+
+                cygwin_exec(isabelle_root,
+                    List.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall"));
+                cygwin_exec(isabelle_root,
+                    List.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall"));
+            }
+        }
+    }
+
+
+    /* implicit settings environment */
+
+    private static volatile Map<String,String> _settings = null;
+
+    public static Map<String,String> settings()
+        throws IOException, InterruptedException
+    {
+        if (_settings == null) { init("", ""); }  // unsynchronized check
+        return _settings;
+    }
+
+    public static String getenv(String name)
+        throws IOException, InterruptedException
+    {
+        return settings().getOrDefault(name, "");
+    }
+
+    public static synchronized void init(String _isabelle_root, String _cygwin_root)
+        throws IOException, InterruptedException
+    {
+        if (_settings == null) {
+            String isabelle_root =
+                bootstrap_directory(_isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root");
+
+            String cygwin_root = "";
+            if (is_windows()) {
+                cygwin_root = bootstrap_directory(_cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root");
+                cygwin_init(isabelle_root, cygwin_root);
+            }
+
+            Map<String,String> env = new HashMap<String,String>(System.getenv());
+
+            BiFunction<String,String,Void> env_default =
+                (String a, String b) -> { if (!b.isEmpty()) env.putIfAbsent(a, b); return null; };
+
+            String temp_windows = is_windows() ? System.getenv("TEMP") : null;
+
+            env_default.apply("CYGWIN_ROOT", cygwin_root);
+            env_default.apply("TEMP_WINDOWS",
+                (temp_windows != null && temp_windows.contains("\\")) ? temp_windows : "");
+            env_default.apply("ISABELLE_JDK_HOME",
+                standard_path(cygwin_root, System.getProperty("java.home", "")));
+            env_default.apply("HOME", System.getProperty("user.home", ""));
+            env_default.apply("ISABELLE_APP", System.getProperty("isabelle.app", ""));
+
+            Map<String,String> settings = new HashMap<String,String>();
+            Path settings_file = Files.createTempFile(null, null);
+            try {
+                List<String> cmd = new LinkedList<String>();
+                if (is_windows()) {
+                    cmd.add(cygwin_root + "\\bin\\bash");
+                    cmd.add("-l");
+                    cmd.add(standard_path(cygwin_root, isabelle_root + "\\bin\\isabelle"));
+                } else {
+                    cmd.add(isabelle_root + "/bin/isabelle");
+                }
+                cmd.add("getenv");
+                cmd.add("-d");
+                cmd.add(settings_file.toString());
+
+                Exec_Result res = exec_process(cmd, null, env, true);
+                if (!res.ok()) throw new RuntimeException(res.out());
+
+                for (String s : Files.readString(settings_file).split("\u0000", -1)) {
+                    int i = s.indexOf('=');
+                    if (i > 0) { settings.put(s.substring(0, i), s.substring(i + 1)); }
+                    else if (i < 0 && !s.isEmpty()) { settings.put(s, ""); }
+                }
+            }
+            finally { Files.delete(settings_file); }
+
+            if (is_windows()) { settings.put("CYGWIN_ROOT", cygwin_root); }
+
+            settings.put("PATH", settings.get("PATH_JVM"));
+            settings.remove("PATH_JVM");
+
+            _settings = Map.copyOf(settings);
+        }
+    }
+
+
+    /* Cygwin root (after init) */
+
+    public static String cygwin_root()
+        throws IOException, InterruptedException
+    {
+        return getenv("CYGWIN_ROOT");
+    }
+
+    public static String standard_path(String platform_path)
+        throws IOException, InterruptedException
+    {
+        return standard_path(cygwin_root(), platform_path);
+    }
+
+    public static String expand_platform_path(String standard_path)
+            throws IOException, InterruptedException
+    {
+        return expand_platform_path(settings(), cygwin_root(), standard_path);
+    }
+
+    public static String platform_path(String standard_path)
+        throws IOException, InterruptedException
+    {
+        return expand_platform_path(null, cygwin_root(), standard_path);
+    }
+
+
+    /* kill process (via bash) */
+
+    static public boolean kill_process(String group_pid, String signal)
+        throws IOException, InterruptedException
+    {
+        List<String> cmd = new LinkedList<String>();
+        if (is_windows()) {
+            cmd.add(cygwin_root() + "\\bin\\bash.exe");
+        }
+        else {
+            cmd.add("/usr/bin/env");
+            cmd.add("bash");
+        }
+        cmd.add("-c");
+        cmd.add("kill -" + signal + " -" + group_pid);
+        return exec_process(cmd, null, null, false).ok();
+    }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/src/Exn.java	Sat Jul 17 21:40:57 2021 +0200
@@ -0,0 +1,83 @@
+/*  Title:      Tools/Setup/src/Exn.java
+    Author:     Makarius
+
+Support for exceptions (arbitrary throwables).
+*/
+
+package isabelle.setup;
+
+
+import java.io.IOException;
+import java.util.LinkedList;
+import java.util.List;
+
+
+public class Exn
+{
+    /* interrupts */
+
+    public static boolean is_interrupt(Throwable exn)
+    {
+        boolean found_interrupt = false;
+        Throwable e = exn;
+        while (!found_interrupt && e != null) {
+            found_interrupt = e instanceof InterruptedException;
+            e = e.getCause();
+        }
+        return found_interrupt;
+    }
+
+    public static int INTERRUPT_RETURN_CODE = 130;
+
+    public static int return_code(Throwable exn, int rc)
+    {
+        return is_interrupt(exn) ? INTERRUPT_RETURN_CODE : rc;
+    }
+
+
+    /* message */
+
+    public static String message(Throwable exn)
+    {
+        String msg = exn.getMessage();
+
+        if (exn.getClass() == RuntimeException.class)
+        {
+            return msg == null || msg.isEmpty() ? "Error" : msg;
+        }
+        else if (exn instanceof IOException)
+        {
+            return msg == null || msg.isEmpty() ? "I/O error" : "I/O error: " + msg;
+        }
+        else if (exn instanceof RuntimeException && !msg.isEmpty()) { return msg; }
+        else if (exn instanceof InterruptedException) { return "Interrupt"; }
+        else { return exn.toString(); }
+    }
+
+
+    /* print */
+
+    public static String trace(Throwable exn)
+    {
+        List<String> list = new LinkedList<String>();
+        for (StackTraceElement elem : exn.getStackTrace()) {
+            list.add(elem.toString());
+        }
+        return Library.cat_lines(list);
+    }
+
+    public static boolean debug()
+    {
+        return System.getProperty("isabelle.debug", "").equals("true");
+    }
+
+    public static String print(Throwable exn)
+    {
+        return debug() ? message(exn) + "\n" + trace(exn) : message(exn);
+    }
+
+    public static String print_error(Throwable exn)
+    {
+        return Library.prefix_lines("*** ", print(exn));
+    }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/src/Library.java	Sat Jul 17 21:40:57 2021 +0200
@@ -0,0 +1,53 @@
+/*  Title:      Tools/Setup/src/Library.java
+    Author:     Makarius
+
+Basic library.
+*/
+
+package isabelle.setup;
+
+
+import java.util.Arrays;
+import java.util.LinkedList;
+import java.util.List;
+
+
+public class Library
+{
+    public static String quote(String s)
+    {
+        return "\"" + s + "\"";
+    }
+
+    public static String cat_lines(Iterable<? extends CharSequence> lines)
+    {
+        return String.join("\n", lines);
+    }
+
+    public static List<String> split_lines(String str)
+    {
+        if (str.isEmpty()) { return List.of(); }
+        else {
+            List<String> result = new LinkedList<String>();
+            result.addAll(Arrays.asList(str.split("\\n")));
+            return List.copyOf(result);
+        }
+    }
+
+    public static String prefix_lines(String prfx, String str)
+    {
+        if (str.isEmpty()) { return str; }
+        else {
+            List<String> lines = new LinkedList<String>();
+            for (String line : split_lines(str)) { lines.add(prfx + line); }
+            return cat_lines(lines);
+        }
+    }
+
+    public static String trim_line(String s)
+    {
+        if (s.endsWith("\r\n")) { return s.substring(0, s.length() - 2); }
+        else if (s.endsWith("\r") || s.endsWith("\n")) { return s.substring(0, s.length() - 1); }
+        else { return s; }
+    }
+}
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/src/Setup.java	Sat Jul 17 21:40:57 2021 +0200
@@ -0,0 +1,65 @@
+/*  Title:      Tools/Setup/src/Setup.java
+    Author:     Makarius
+
+Isabelle setup tool: bootstrap from generic Java environment.
+*/
+
+package isabelle.setup;
+
+
+class Setup
+{
+    private static void echo(String msg)
+    {
+        System.out.print(msg + "\n");
+    }
+    private static void echo_err(String msg)
+    {
+        System.err.print(msg + "\n");
+    }
+    private static void fail(String msg)
+    {
+        echo_err(msg);
+        System.exit(2);
+    }
+
+    private static void check_args(boolean b)
+    {
+        if (!b) { fail("Bad command-line arguments"); }
+    }
+
+    public static void main(String[] args)
+    {
+        int n = args.length;
+        check_args(n > 0);
+
+        String op = args[0];
+        try {
+            switch (op) {
+                case "build":
+                    check_args(n == 1);
+                    Build.build_components(false);
+                    break;
+                case "build_fresh":
+                    check_args(n == 1);
+                    Build.build_components(true);
+                    break;
+                case "classpath":
+                    check_args(n == 1);
+                    echo(Environment.join_standard_paths(Build.classpath()));
+                    break;
+                case "services":
+                    check_args(n == 1);
+                    for (String s : Build.services()) { echo(s); }
+                    break;
+                default:
+                    fail("Bad setup operation " + Library.quote(op));
+                    break;
+            }
+        }
+        catch (Throwable exn) {
+            echo_err(Exn.print_error(exn));
+            System.exit(Exn.return_code(exn, 2));
+        }
+    }
+}