clarified build_props: empty module means no build;
clarified signature;
clarified errors;
--- a/Admin/components/components.sha1 Sat Jul 17 12:59:47 2021 +0200
+++ b/Admin/components/components.sha1 Sat Jul 17 13:42:21 2021 +0200
@@ -128,6 +128,7 @@
d2c9fd7b73457a460111edd6eb93a133272935fb isabelle_setup-20210715.tar.gz
a5f478ba1088f67c2c86dc2fa7764b6d884e5ae5 isabelle_setup-20210716-1.tar.gz
79fad009cb22aa5e7cb4aed3c810ad5f61790293 isabelle_setup-20210716.tar.gz
+14f8508bcae9140815bb23e430e26d2cbc504b81 isabelle_setup-20210717.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
--- a/Admin/components/main Sat Jul 17 12:59:47 2021 +0200
+++ b/Admin/components/main Sat Jul 17 13:42:21 2021 +0200
@@ -8,7 +8,7 @@
flatlaf-1.2
idea-icons-20210508
isabelle_fonts-20210322
-isabelle_setup-20210716-1
+isabelle_setup-20210717
jdk-15.0.2+7
jedit-20210715
jfreechart-1.5.1
--- a/Admin/etc/build.props Sat Jul 17 12:59:47 2021 +0200
+++ b/Admin/etc/build.props Sat Jul 17 13:42:21 2021 +0200
@@ -1,4 +1,3 @@
-description = Isabelle/Scala/Admin
-lib = $ISABELLE_HOME/lib/classes
-name = isabelle_admin
+title = Isabelle/Scala/Admin
+module = $ISABELLE_HOME/lib/classes/isabelle_admin.jar
services = isabelle.Admin_Tools
--- a/etc/build.props Sat Jul 17 12:59:47 2021 +0200
+++ b/etc/build.props Sat Jul 17 13:42:21 2021 +0200
@@ -1,6 +1,5 @@
-description = Isabelle/Scala
-lib = lib/classes
-name = isabelle
+title = Isabelle/Scala
+module = $ISABELLE_HOME/lib/classes/isabelle.jar
main = isabelle.jedit.Main
resources = \
lib/services/java.nio.charset.spi.CharsetProvider:META-INF/services/ \
--- a/src/Tools/GraphBrowser/etc/build.props Sat Jul 17 12:59:47 2021 +0200
+++ b/src/Tools/GraphBrowser/etc/build.props Sat Jul 17 13:42:21 2021 +0200
@@ -1,6 +1,5 @@
-description = graph browser
-lib = $ISABELLE_HOME/lib/classes
-name = isabelle_graphbrowser
+title = graph browser
+module = $ISABELLE_HOME/lib/classes/isabelle_graphbrowser.jar
javac_options = -source 7 -target 7
sources = \
awt/Border.java \
--- a/src/Tools/Setup/isabelle/setup/Build.java Sat Jul 17 12:59:47 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build.java Sat Jul 17 13:42:21 2021 +0200
@@ -55,17 +55,18 @@
throws IOException
{
Properties props = new Properties();
- props.load(Files.newBufferedReader(dir.resolve(BUILD_PROPS)));
- return new Context(dir, props);
+ 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 build_props = dir.resolve(COMPONENT_BUILD_PROPS);
- if (Files.exists(build_props)) { props.load(Files.newBufferedReader(build_props)); }
- return new Context(dir, props);
+ 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()
@@ -93,24 +94,36 @@
{
private final Path _dir;
private final Properties _props;
+ private final String _location;
- public Context(Path dir, Properties props)
+ public Context(Path dir, Properties props, String location)
{
_dir = dir;
_props = props;
+ _location = location;
}
@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 error_message(String msg)
+ {
+ if (_location == null || _location.isEmpty()) {
+ return msg;
+ }
+ else {
+ return msg +" (in " + Library.quote(_location) + ")";
+ }
+ }
- public String lib_name() { return _props.getProperty("lib", "lib") + "/" + name(); }
- public String jar_name() { return lib_name() + ".jar"; }
+ public String title() {
+ String title = _props.getProperty("title", "");
+ if (title.isEmpty()) { throw new RuntimeException(error_message("Missing title")); }
+ else return title;
+ }
+ public String module() { return _props.getProperty("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)
@@ -164,7 +177,7 @@
}
else {
throw new RuntimeException(
- "Missing input file " + Environment.quote(file.toString()));
+ error_message("Missing input file " + Library.quote(file.toString())));
}
}
return sha_digest(sha, name);
@@ -393,7 +406,8 @@
{
List<Path> result = new LinkedList<Path>();
for (Context context : component_contexts()) {
- result.add(context.path(context.jar_name()));
+ String module = context.module();
+ if (!module.isEmpty()) { result.add(context.path(module)); }
}
return List.copyOf(result);
}
@@ -416,108 +430,116 @@
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);
+ String module = context.module();
+ if (!module.isEmpty()) {
+ String title = context.title();
- List<String> requirements = context.requirements();
- List<String> resources = context.resources();
- List<String> sources = context.sources();
+ 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();
- if (context.is_vacuous()) { 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();
- _shasum.append(context.shasum_props());
- 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);
+ 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) {
+ 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.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)));
}
}
- _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.print(
- "### Building " + context.description() + " (" + jar_path + ") ...\n");
- String isabelle_class_path = Environment.getenv("ISABELLE_CLASSPATH");
+ List<Path> compiler_sources = new LinkedList<Path>();
+ for (String s : sources) { compiler_sources.add(context.path(s)); }
- 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)));
- }
- }
+ compile_scala_sources(
+ build_dir, context.scalac_options(), compiler_deps, compiler_sources);
- 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);
+ compiler_deps.add(build_dir);
+ compile_java_sources(
+ build_dir, context.javac_options(), compiler_deps, compiler_sources);
- /* copy resources */
+ /* 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();
+ 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);
+ 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();
+ }
}
- 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);
}
- Files.createDirectories(target_dir);
- Files.copy(context.path(name), target_file,
- StandardCopyOption.COPY_ATTRIBUTES);
- }
- /* packaging */
+ /* 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);
+ 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);
+ }
}
}
}
--- a/src/Tools/Setup/isabelle/setup/Environment.java Sat Jul 17 12:59:47 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Environment.java Sat Jul 17 13:42:21 2021 +0200
@@ -30,11 +30,6 @@
return System.getProperty("os.name", "").startsWith("Windows");
}
- public static String quote(String s)
- {
- return "\"" + s + "\"";
- }
-
/* system path representations */
@@ -139,7 +134,7 @@
String res = env.getOrDefault(var, "");
if (res.isEmpty()) {
throw new RuntimeException(
- "Bad Isabelle environment variable: " + quote(var));
+ "Bad Isabelle environment variable: " + Library.quote(var));
}
else check(null, res);
}
@@ -275,7 +270,9 @@
else { throw new RuntimeException("Unknown " + description + " directory"); }
if ((new File(dir)).isDirectory()) { return dir; }
- else { throw new RuntimeException("Bad " + description + " directory " + quote(dir)); }
+ else {
+ throw new RuntimeException("Bad " + description + " directory " + Library.quote(dir));
+ }
}
private static void cygwin_exec(String isabelle_root, List<String> cmd)
--- a/src/Tools/Setup/isabelle/setup/Library.java Sat Jul 17 12:59:47 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Library.java Sat Jul 17 13:42:21 2021 +0200
@@ -14,6 +14,11 @@
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);
--- a/src/Tools/Setup/isabelle/setup/Setup.java Sat Jul 17 12:59:47 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Setup.java Sat Jul 17 13:42:21 2021 +0200
@@ -53,7 +53,7 @@
for (String s : Build.services()) { echo(s); }
break;
default:
- fail("Bad setup operation " + Environment.quote(op));
+ fail("Bad setup operation " + Library.quote(op));
break;
}
}
--- a/src/Tools/jEdit/jedit_base/build.props Sat Jul 17 12:59:47 2021 +0200
+++ b/src/Tools/jEdit/jedit_base/build.props Sat Jul 17 13:42:21 2021 +0200
@@ -1,6 +1,5 @@
-description = Isabelle/jEdit base plugin
-lib = $JEDIT_SETTINGS/jars
-name = isabelle_jedit_base
+title = Isabelle/jEdit base plugin
+module = $JEDIT_SETTINGS/jars/isabelle_jedit_base.jar
requirements = \
env:ISABELLE_SCALA_JAR \
env:JEDIT_JARS
--- a/src/Tools/jEdit/jedit_main/build.props Sat Jul 17 12:59:47 2021 +0200
+++ b/src/Tools/jEdit/jedit_main/build.props Sat Jul 17 13:42:21 2021 +0200
@@ -1,6 +1,5 @@
-description = Isabelle/jEdit main plugin
-lib = $JEDIT_SETTINGS/jars
-name = isabelle_jedit_main
+title = Isabelle/jEdit main plugin
+module = $JEDIT_SETTINGS/jars/isabelle_jedit_main.jar
requirements = \
env:ISABELLE_SCALA_JAR \
env:JEDIT_JARS