--- a/Admin/components/components.sha1 Fri Jul 09 17:59:25 2021 +0200
+++ b/Admin/components/components.sha1 Fri Jul 09 21:24:28 2021 +0200
@@ -123,6 +123,7 @@
1f7a0b9829ecac6552b21e995ad0f0ac168634f3 isabelle_fonts-20210322.tar.gz
916adccd2f40c55116b68b92ce1eccb24d4dd9a2 isabelle_setup-20210630.tar.gz
c611e363287fcc9bdd93c33bef85fa4e66cd3f37 isabelle_setup-20210701.tar.gz
+a0e7527448ef0f7ce164a38a50dc26e98de3cad6 isabelle_setup-20210709.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
@@ -210,6 +211,7 @@
0bdbd36eda5992396e9c6b66aa24259d4dd7559c jedit_build-20210201.tar.gz
a0744f1948abdde4bfb51dd4769b619e7444baf1 jedit_build-20210510-1.tar.gz
837d6c8f72ecb21ad59a2544c69aadc9f05684c6 jedit_build-20210510.tar.gz
+7bdae3d24b10261f6cb277446cf9ecab6062bd6f jedit_build-20210708.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz
--- a/Admin/components/main Fri Jul 09 17:59:25 2021 +0200
+++ b/Admin/components/main Fri Jul 09 21:24:28 2021 +0200
@@ -8,9 +8,9 @@
flatlaf-1.2
idea-icons-20210508
isabelle_fonts-20210322
-isabelle_setup-20210701
+isabelle_setup-20210709
jdk-15.0.2+7
-jedit_build-20210510-1
+jedit_build-20210708
jfreechart-1.5.1
jortho-1.0-2
kodkodi-1.5.6-1
--- a/Admin/lib/Tools/build_setup Fri Jul 09 17:59:25 2021 +0200
+++ b/Admin/lib/Tools/build_setup Fri Jul 09 21:24:28 2021 +0200
@@ -7,7 +7,7 @@
## sources
declare -a SOURCES=(
- "Build_Scala.java"
+ "Build.java"
"Environment.java"
"Setup.java"
)
@@ -57,7 +57,8 @@
ARGS["${#ARGS[@]}"]="$(platform_path "$ISABELLE_HOME/src/Tools/Setup/isabelle/setup/$SRC")"
done
-isabelle_jdk javac -d "$TARGET_DIR" -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "${ARGS[@]}" || \
+isabelle_jdk javac $ISABELLE_JAVAC_OPTIONS -d "$TARGET_DIR" \
+ -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "${ARGS[@]}" || \
fail "Failed to compile sources"
isabelle_jdk jar -c -f "$(platform_path "$TARGET_DIR/isabelle_setup.jar")" \
--- a/etc/settings Fri Jul 09 17:59:25 2021 +0200
+++ b/etc/settings Fri Jul 09 21:24:28 2021 +0200
@@ -16,6 +16,7 @@
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
+ISABELLE_JAVAC_OPTIONS="-encoding UTF-8 -Xlint:-options -deprecation -source 11 -target 11"
ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -Wconf:cat=other-match-analysis:silent -feature -deprecation -target:11 -Xsource:3 -J-Xms512m -J-Xmx4g -J-Xss16m"
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
--- a/src/Pure/Admin/build_jedit.scala Fri Jul 09 17:59:25 2021 +0200
+++ b/src/Pure/Admin/build_jedit.scala Fri Jul 09 21:24:28 2021 +0200
@@ -614,9 +614,10 @@
File.write(etc_dir + Path.explode("settings"),
"""# -*- shell-script -*- :mode=shellscript:
-ISABELLE_JEDIT_BUILD_HOME="$COMPONENT"
-ISABELLE_JEDIT_BUILD_VERSION=""" + quote(jedit_patched) + """
-""")
+ISABELLE_JEDIT_HOME="$COMPONENT/""" + jedit_patched + """"
+ISABELLE_JEDIT_JARS=""" +
+ File.read_dir(jars_dir).map("$ISABELLE_JEDIT_HOME/jars/" + _).mkString("\"", ":", "\"\n")
+)
/* README */
--- a/src/Pure/Admin/isabelle_cronjob.scala Fri Jul 09 17:59:25 2021 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Fri Jul 09 21:24:28 2021 +0200
@@ -58,7 +58,7 @@
Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check
if (!Isabelle_Devel.cronjob_log.is_file)
- Files.createSymbolicLink(Isabelle_Devel.cronjob_log.file.toPath, current_log.file.toPath)
+ Files.createSymbolicLink(Isabelle_Devel.cronjob_log.java_path, current_log.java_path)
})
val exit: Logger_Task =
--- a/src/Pure/General/file.scala Fri Jul 09 17:59:25 2021 +0200
+++ b/src/Pure/General/file.scala Fri Jul 09 21:24:28 2021 +0200
@@ -68,8 +68,8 @@
def relative_path(base: Path, other: Path): Option[Path] =
{
- val base_path = base.file.toPath
- val other_path = other.file.toPath
+ val base_path = base.java_path
+ val other_path = other.java_path
if (other_path.startsWith(base_path))
Some(path(base_path.relativize(other_path).toFile))
else None
--- a/src/Pure/General/path.scala Fri Jul 09 17:59:25 2021 +0200
+++ b/src/Pure/General/path.scala Fri Jul 09 21:24:28 2021 +0200
@@ -10,6 +10,7 @@
import java.util.{Map => JMap}
import java.io.{File => JFile}
+import java.nio.file.{Path => JPath}
import scala.util.matching.Regex
@@ -306,6 +307,8 @@
def is_file: Boolean = file.isFile
def is_dir: Boolean = file.isDirectory
+ def java_path: JPath = file.toPath
+
def absolute_file: JFile = File.absolute(file)
def canonical_file: JFile = File.canonical(file)
--- a/src/Pure/System/isabelle_system.scala Fri Jul 09 17:59:25 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala Fri Jul 09 21:24:28 2021 +0200
@@ -153,7 +153,7 @@
def make_directory(path: Path): Path =
{
if (!path.is_dir) {
- try { Files.createDirectories(path.file.toPath) }
+ try { Files.createDirectories(path.java_path) }
catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
}
path
--- a/src/Pure/Thy/sessions.scala Fri Jul 09 17:59:25 2021 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Jul 09 21:24:28 2021 +0200
@@ -1144,7 +1144,7 @@
def read_heap_digest(heap: Path): Option[String] =
{
if (heap.is_file) {
- using(FileChannel.open(heap.file.toPath, StandardOpenOption.READ))(file =>
+ using(FileChannel.open(heap.java_path, StandardOpenOption.READ))(file =>
{
val len = file.size
val n = sha1_prefix.length + SHA1.digest_length
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/isabelle/setup/Build.java Fri Jul 09 21:24:28 2021 +0200
@@ -0,0 +1,404 @@
+/* Title: Tools/Setup/isabelle/setup/Build.java
+ Author: Makarius
+
+Build Isabelle/Scala/Java modules.
+*/
+
+package isabelle.setup;
+
+
+import java.io.BufferedOutputStream;
+import java.io.File;
+import java.io.IOException;
+import java.math.BigInteger;
+import java.nio.charset.StandardCharsets;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.StandardCopyOption;
+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.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 Context directory_context(Path dir)
+ throws IOException
+ {
+ Properties props = new Properties();
+ props.load(Files.newBufferedReader(dir.resolve(BUILD_PROPS)));
+ return new Context(dir, props);
+ }
+
+ public static Context component_context(Path dir)
+ throws IOException
+ {
+ Properties props = new Properties();
+ Path build_props = dir.resolve("etc").resolve(BUILD_PROPS);
+ if (Files.exists(build_props)) { props.load(Files.newBufferedReader(build_props)); }
+ return new Context(dir, props);
+ }
+
+ public static class Context
+ {
+ private final Path _dir;
+ private final Properties _props;
+
+ public Context(Path dir, Properties props)
+ {
+ _dir = dir;
+ _props = props;
+ }
+
+ @Override public String toString() { return _dir.toString(); }
+
+ public String name() { return _props.getProperty("name", _dir.toFile().getName()); }
+ public String description() { return _props.getProperty("description", name()); }
+
+ public String lib_name() { return _props.getProperty("lib", "lib") + "/" + name(); }
+ public String jar_name() { return lib_name() + ".jar"; }
+
+ 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 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));
+ }
+
+ // historic
+ public Path shasum_path()
+ throws IOException, InterruptedException
+ {
+ return path(lib_name() + ".shasum");
+ }
+
+ 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
+ {
+ boolean exists = false;
+ MessageDigest sha = MessageDigest.getInstance("SHA");
+ for (Path file : paths) {
+ if (Files.exists(file)) {
+ exists = true;
+ sha.update(Files.readAllBytes(file));
+ }
+ }
+ if (exists) {
+ String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest()));
+ return digest + " " + name + "\n";
+ }
+ else { return ""; }
+ }
+
+ public String shasum(String file)
+ throws IOException, NoSuchAlgorithmException, InterruptedException
+ {
+ return shasum(file, List.of(path(file)));
+ }
+ }
+
+
+ /** 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); }
+ }
+ }
+ }
+
+ 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_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) {
+ MainClass main = new MainClass();
+ boolean ok = main.process(args.toArray(String[]::new));
+ if (!ok) throw new RuntimeException("Failed to compile 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_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()) {
+ boolean ok = compiler.getTask(null, file_manager, null, options, null, java_sources).call();
+ if (!ok) throw new RuntimeException("Failed to compile Java sources");
+ }
+ }
+
+
+ /** shasum for jar content **/
+
+ private static String SHASUM = "META-INF/shasum";
+
+ public static String get_shasum(Path jar_path)
+ throws IOException
+ {
+ if (Files.exists(jar_path)) {
+ try (JarFile jar_file = new JarFile(jar_path.toFile()))
+ {
+ JarEntry entry = jar_file.getJarEntry(SHASUM);
+ if (entry != null) {
+ byte[] bytes = jar_file.getInputStream(entry).readAllBytes();
+ return new String(bytes, StandardCharsets.UTF_8);
+ }
+ else { return ""; }
+ }
+ }
+ else { return ""; }
+ }
+
+ public static void create_shasum(Path dir, String shasum)
+ throws IOException
+ {
+ Path path = dir.resolve(SHASUM);
+ Files.createDirectories(path.getParent());
+ Files.writeString(path, shasum);
+ }
+
+
+ /** 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();
+ }
+ }
+ }
+ }
+ }
+
+
+ /** build **/
+
+ public static void build(Context context, boolean fresh)
+ throws IOException, InterruptedException, NoSuchAlgorithmException
+ {
+ String jar_name = context.jar_name();
+ Path jar_path = context.path(jar_name);
+
+ List<String> requirements = context.requirements();
+ List<String> resources = context.resources();
+ List<String> sources = context.sources();
+
+ Files.deleteIfExists(context.shasum_path());
+
+ if (sources.isEmpty() && resources.isEmpty()) {
+ Files.deleteIfExists(jar_path);
+ }
+ else {
+ String shasum_old = get_shasum(jar_path);
+ String shasum;
+ List<Path> compiler_deps = new LinkedList<Path>();
+ {
+ StringBuilder _shasum = new StringBuilder();
+ for (String s : requirements) {
+ 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));
+ compiler_deps.add(path);
+ paths.add(path);
+ }
+ }
+ _shasum.append(context.shasum(s, paths));
+ }
+ else {
+ compiler_deps.add(context.path(s));
+ _shasum.append(context.shasum(s));
+ }
+ }
+ 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.println(
+ "### Building " + context.description() + " (" + jar_path + ") ...");
+
+ String isabelle_class_path = Environment.getenv("ISABELLE_CLASSPATH");
+
+ Path build_dir = Files.createTempDirectory("isabelle");
+ try {
+ /* compile sources */
+
+ for (String s : isabelle_class_path.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_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);
+ }
+ }
+ }
+ }
+ }
+}
--- a/src/Tools/Setup/isabelle/setup/Build_Scala.java Fri Jul 09 17:59:25 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,255 +0,0 @@
-/* Title: Tools/Setup/isabelle/setup/Build_Scala.java
- Author: Makarius
-
-Build Isabelle/Scala modules.
-*/
-
-package isabelle.setup;
-
-
-import java.io.BufferedOutputStream;
-import java.io.File;
-import java.io.IOException;
-import java.math.BigInteger;
-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.jar.Attributes;
-import java.util.jar.JarEntry;
-import java.util.jar.JarOutputStream;
-import java.util.jar.Manifest;
-import java.util.stream.Stream;
-
-import scala.tools.nsc.MainClass;
-
-
-public class Build_Scala
-{
- /** component directory context **/
-
- public static class Context
- {
- private final Path component_dir;
- private Properties props;
-
- public Context(Path dir) throws IOException
- {
- component_dir = dir;
- props = new Properties();
- Path path = component_dir.resolve("etc/scala.props");
- if (Files.exists(path)) { props.load(Files.newBufferedReader(path)); }
- }
-
- @Override public String toString() { return component_dir.toString(); }
-
- public String component_name() { return component_dir.toFile().getName(); }
- public String name() { return props.getProperty("name", component_name()); }
- public String description() { return props.getProperty("description", name()); }
-
- public String lib_name() { return props.getProperty("lib", "lib") + "/" + name(); }
- public String jar_name() { return lib_name() + ".jar"; }
- public String shasum_name() { return lib_name() + ".shasum"; }
-
- public String main() { return props.getProperty("main", ""); }
-
- 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> sources() { return get_list("sources"); }
- public List<String> resources() { return get_list("resources"); }
- public List<String> services() { return get_list("services"); }
-
- public Path path(String file) { return component_dir.resolve(file); }
- public boolean exists(String file) { return Files.exists(path(file)); }
-
- 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 file)
- throws IOException, NoSuchAlgorithmException
- {
- if (exists(file)) {
- MessageDigest sha = MessageDigest.getInstance("SHA");
- sha.update(Files.readAllBytes(path(file)));
- String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest()));
- return digest + " *" + file + "\n";
- }
- else { return ""; }
- }
- }
-
-
- /** compile sources **/
-
- public static void compile_sources(
- Path target_dir, List<Path> deps, String options, List<Path> sources)
- {
- ArrayList<String> args = new ArrayList<String>();
- args.add("-d");
- args.add(target_dir.toString());
- args.add("-bootclasspath");
- args.add(Environment.join_paths(deps));
- for (String s : options.split("\\s+")) {
- if (!s.isEmpty()) { args.add(s); }
- }
- args.add("--");
- for (Path p : sources) { args.add(p.toString()); }
-
- MainClass main = new MainClass();
- boolean ok = main.process(args.toArray(String[]::new));
- if (!ok) throw new RuntimeException("Failed to compile sources");
- }
-
-
- /** create jar **/
-
- public static void create_jar(Path dir, String main, Path jar)
- throws IOException
- {
- Files.deleteIfExists(jar);
-
- Manifest manifest = new Manifest();
- Attributes attributes = manifest.getMainAttributes();
- attributes.put(Attributes.Name.MANIFEST_VERSION, "1.0");
- attributes.put(new Attributes.Name("Created-By"),
- System.getProperty("java.version") + " (" + System.getProperty("java.vendor") + ")");
- if (!main.isEmpty()) { attributes.put(Attributes.Name.MAIN_CLASS, main); }
-
- try (JarOutputStream out =
- new JarOutputStream(new BufferedOutputStream(Files.newOutputStream(jar)), manifest))
- {
- for (Path path : Files.walk(dir).sorted().toArray(Path[]::new)) {
- boolean is_dir = Files.isDirectory(path);
- boolean is_file = Files.isRegularFile(path);
- if (is_dir || is_file) {
- String name = Environment.slashes(dir.relativize(path).toString());
- JarEntry entry = new JarEntry(is_dir ? name + "/" : name);
- entry.setTime(path.toFile().lastModified());
- out.putNextEntry(entry);
- if (is_file) { out.write(Files.readAllBytes(path)); }
- out.closeEntry();
- }
- }
- }
- }
-
-
-
- /** build scala **/
-
- public static void build_scala(Context context, boolean fresh)
- throws IOException, InterruptedException, NoSuchAlgorithmException
- {
- String jar_name = context.jar_name();
- Path jar_path = context.path(jar_name);
- String shasum_name = context.shasum_name();
-
- List<String> sources = context.sources();
- List<String> resources = context.resources();
-
- if (sources.isEmpty()) {
- Files.deleteIfExists(jar_path);
- Files.deleteIfExists(context.path(shasum_name));
- }
- else {
- String shasum_old =
- context.exists(shasum_name) ? Files.readString(context.path(shasum_name)) : "";
- String shasum_sources;
- {
- StringBuilder _shasum = new StringBuilder();
- for (String s : resources) {
- _shasum.append(context.shasum(context.item_name(s)));
- }
- for (String s : sources) { _shasum.append(context.shasum(s)); }
- shasum_sources = _shasum.toString();
- }
- if (fresh || !shasum_old.equals(context.shasum(jar_name) + shasum_sources)) {
- System.out.println(
- "### Building " + context.description() + " (" + jar_path + ") ...");
-
- String scalac_options = Environment.getenv("ISABELLE_SCALAC_OPTIONS");
- String isabelle_class_path = Environment.getenv("ISABELLE_CLASSPATH");
-
- Path build_dir = Files.createTempDirectory("isabelle");
- try {
- /* compile sources */
-
- List<Path> compiler_deps = new LinkedList<Path>();
- for (String s : isabelle_class_path.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_sources(build_dir, compiler_deps, scalac_options, 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_jar(build_dir, context.main(), jar_path);
-
- String shasum = context.shasum(jar_name) + shasum_sources;
- Files.writeString(context.path(shasum_name), shasum);
- }
- finally {
- try (Stream<Path> walk = Files.walk(build_dir)) {
- walk.sorted(Comparator.reverseOrder())
- .map(Path::toFile)
- .forEach(File::delete);
- }
- }
- }
- }
- }
-}
--- a/src/Tools/Setup/isabelle/setup/Environment.java Fri Jul 09 17:59:25 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Environment.java Fri Jul 09 21:24:28 2021 +0200
@@ -67,50 +67,103 @@
else { return platform_path; }
}
- public static String platform_path(String cygwin_root, String standard_path)
+ private static class Expand_Platform_Path
{
- if (is_windows()) {
- StringBuilder result_path = new StringBuilder();
+ private String _cygwin_root;
+ private StringBuilder _result = new StringBuilder();
- Pattern cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)");
- Matcher cygdrive_matcher = cygdrive_pattern.matcher(standard_path);
+ public Expand_Platform_Path(String cygwin_root)
+ {
+ _cygwin_root = cygwin_root;
+ }
- Pattern named_root_pattern = Pattern.compile("//+([^/]*)(.*)");
- Matcher named_root_matcher = named_root_pattern.matcher(standard_path);
+ public String result() { return _result.toString(); }
- String rest;
- if (cygdrive_matcher.matches()) {
- String drive = cygdrive_matcher.group(1).toUpperCase(Locale.ROOT);
- rest = cygdrive_matcher.group(2);
- result_path.append(drive);
- result_path.append(':');
- result_path.append(File.separatorChar);
+ 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);
}
- else if (named_root_matcher.matches()) {
- String root = named_root_matcher.group(1);
- rest = named_root_matcher.group(2);
- result_path.append(File.separatorChar);
- result_path.append(File.separatorChar);
- result_path.append(root);
- }
- else {
- if (standard_path.startsWith("/")) { result_path.append(cygwin_root); }
- rest = standard_path;
- }
+ }
+
+ 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);
- for (String p : rest.split("/", -1)) {
- if (!p.isEmpty()) {
- int len = result_path.length();
- if (len > 0 && result_path.charAt(len - 1) != File.separatorChar) {
- result_path.append(File.separatorChar);
- }
- result_path.append(p);
+ 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;
+ }
- return result_path.toString();
+ 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: " + quote(var));
+ }
+ else check(null, res);
+ }
+ else if (!p.isEmpty()) {
+ separator();
+ add(p);
+ }
+ }
}
- else { return standard_path; }
+
+ 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_paths(List<Path> paths)
@@ -362,10 +415,16 @@
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 platform_path(cygwin_root(), standard_path);
+ return expand_platform_path(null, cygwin_root(), standard_path);
}
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Jul 09 17:59:25 2021 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Jul 09 21:24:28 2021 +0200
@@ -257,12 +257,11 @@
declare -a TARGET_DEPS=("lib/classes/Pure.jar" "$TARGET_DIR/jedit.jar")
-if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
- for DEP in "$ISABELLE_JEDIT_BUILD_HOME/$ISABELLE_JEDIT_BUILD_VERSION"/jars/*.jar
- do
- TARGET_DEPS["${#TARGET_DEPS[@]}"]="$TARGET_DIR/jars/$(basename "$DEP")"
- done
-fi
+splitarray ":" "$ISABELLE_JEDIT_JARS"
+for DEP in "${SPLITARRAY[@]}"
+do
+ TARGET_DEPS["${#TARGET_DEPS[@]}"]="$TARGET_DIR/jars/$(basename "$DEP")"
+done
function target_shasum()
(
@@ -315,13 +314,10 @@
if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then
echo "### Building Isabelle/jEdit ..."
- [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
- fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
-
target_clean || failed
mkdir -p "$TARGET_DIR" || failed
- cp -p -R "$ISABELLE_JEDIT_BUILD_HOME/$ISABELLE_JEDIT_BUILD_VERSION/." "$TARGET_DIR/."
+ cp -p -R "$ISABELLE_JEDIT_HOME/." "$TARGET_DIR/."
init_resources "${RESOURCES0[@]}"
compile_sources "${SOURCES0[@]}"
--- a/src/Tools/jEdit/src/plugin.scala Fri Jul 09 17:59:25 2021 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Fri Jul 09 21:24:28 2021 +0200
@@ -496,3 +496,4 @@
PIDE.editor.shutdown()
}
}
+