--- a/Admin/components/components.sha1 Sat Jul 24 15:38:41 2021 +0200
+++ b/Admin/components/components.sha1 Sat Jul 24 16:40:10 2021 +0200
@@ -132,6 +132,7 @@
7322d6d84d75c486a58ed36630431db4499e3232 isabelle_setup-20210717-2.tar.gz
14f8508bcae9140815bb23e430e26d2cbc504b81 isabelle_setup-20210717.tar.gz
ca801d5c380ea896ee32b309ff19ae5f34538963 isabelle_setup-20210718.tar.gz
+127a75ae33e97480d352087fcb9b47a632d77169 isabelle_setup-20210724.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
@@ -177,6 +178,7 @@
caa0cf65481b6207f66437576643f41dabae3c83 jdk-8u92.tar.gz
778fd85c827ec49d2d658a832d20e63916186b0d jedit-20210715.tar.gz
beb99f2cb0bd4e595c5c597d3970c46aa21616e4 jedit-20210717.tar.gz
+33dd96cd83f2c6a26c035b7a0ee57624655224c5 jedit-20210724.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
--- a/Admin/components/main Sat Jul 24 15:38:41 2021 +0200
+++ b/Admin/components/main Sat Jul 24 16:40:10 2021 +0200
@@ -8,9 +8,9 @@
flatlaf-1.2
idea-icons-20210508
isabelle_fonts-20210322
-isabelle_setup-20210718
+isabelle_setup-20210724
jdk-15.0.2+7
-jedit-20210717
+jedit-20210724
jfreechart-1.5.1
jortho-1.0-2
kodkodi-1.5.6-1
--- a/src/Doc/System/Scala.thy Sat Jul 24 15:38:41 2021 +0200
+++ b/src/Doc/System/Scala.thy Sat Jul 24 16:40:10 2021 +0200
@@ -165,15 +165,16 @@
in printed messages.
\<^item> \<^verbatim>\<open>module\<close> specifies a \<^verbatim>\<open>jar\<close> file name for the output module, as result
- of compiling the specified sources (and resources). If this is absent,
- there is no build process, but contributing sources may still be given,
- possibly together with \<^verbatim>\<open>no_module\<close> as described below.
+ of the specified sources (and resources). If this is absent (or
+ \<^verbatim>\<open>no_build\<close> is set, as described below), there is no implicit build
+ process. The contributing sources might be given nonetheless, notably for
+ @{tool scala_project} (\secref{sec:tool-scala-project}), which includes
+ Scala/Java sources of components, while suppressing \<^verbatim>\<open>jar\<close> modules (to
+ avoid duplication of program content).
- \<^item> \<^verbatim>\<open>no_module\<close> means that there is no build process, but the specified
- \<^verbatim>\<open>jar\<close> is provided by other means. This is relevant for @{tool
- scala_project} (\secref{sec:tool-scala-project}), which includes all
- Scala/Java sources of components, but suppresses \<^verbatim>\<open>jar\<close> modules to avoid
- duplication of content.
+ \<^item> \<^verbatim>\<open>no_build\<close> is a Boolean property, with default \<^verbatim>\<open>false\<close>. If set to
+ \<^verbatim>\<open>true\<close>, the implicit build process for the given \<^verbatim>\<open>module\<close> is \<^emph>\<open>omitted\<close>
+ --- it is assumed to be provided by other means.
\<^item> \<^verbatim>\<open>scalac_options\<close> and \<^verbatim>\<open>javac_options\<close> augment the default settings
@{setting_ref ISABELLE_SCALAC_OPTIONS} and @{setting_ref
--- a/src/Pure/Admin/build_jedit.scala Sat Jul 24 15:38:41 2021 +0200
+++ b/src/Pure/Admin/build_jedit.scala Sat Jul 24 16:40:10 2021 +0200
@@ -191,7 +191,8 @@
})
File.write(etc_dir + Path.explode("build.props"),
- "no_module = " + jedit_patched + "/jedit.jar\n" +
+ "module = " + jedit_patched + "/jedit.jar\n" +
+ "no_build = true\n" +
"requirements = env:JEDIT_JARS\n" +
("sources =" :: java_sources.map(p => " " + p.implode)).mkString("", " \\\n", "\n"))
})
--- a/src/Pure/Tools/scala_build.scala Sat Jul 24 15:38:41 2021 +0200
+++ b/src/Pure/Tools/scala_build.scala Sat Jul 24 16:40:10 2021 +0200
@@ -17,9 +17,11 @@
{
class Context private[Scala_Build](java_context: isabelle.setup.Build.Context)
{
+ override def toString: String = java_context.toString
+
def is_module(path: Path): Boolean =
{
- val module_name: String = java_context.module_name()
+ val module_name = java_context.module_name()
module_name.nonEmpty && File.eq(java_context.path(module_name).toFile, path.file)
}
@@ -38,7 +40,8 @@
def context(dir: Path,
component: Boolean = false,
- more_props: Properties.T = Nil): Context =
+ do_build: Boolean = false,
+ module: Option[Path] = None): Context =
{
val props_name =
if (component) isabelle.setup.Build.COMPONENT_BUILD_PROPS
@@ -47,7 +50,8 @@
val props = new JProperties
props.load(Files.newBufferedReader(props_path.java_path))
- for ((a, b) <- more_props) props.put(a, b)
+ if (do_build) props.remove(isabelle.setup.Build.NO_BUILD)
+ if (module.isDefined) props.put(isabelle.setup.Build.MODULE, File.standard_path(module.get))
new Context(new isabelle.setup.Build.Context(dir.java_path, props, props_path.implode))
}
@@ -55,9 +59,10 @@
def build(dir: Path,
fresh: Boolean = false,
component: Boolean = false,
- more_props: Properties.T = Nil): Unit =
+ do_build: Boolean = false,
+ module: Option[Path] = None): Unit =
{
- context(dir, component = component, more_props = more_props).build(fresh = fresh)
+ context(dir, component = component, do_build = do_build, module = module).build(fresh = fresh)
}
def component_contexts(): List[Context] =
--- a/src/Tools/Setup/etc/build.props Sat Jul 24 15:38:41 2021 +0200
+++ b/src/Tools/Setup/etc/build.props Sat Jul 24 16:40:10 2021 +0200
@@ -1,4 +1,5 @@
-no_module = $ISABELLE_SETUP_JAR
+module = $ISABELLE_SETUP_JAR
+no_build = true
sources = \
src/Build.java \
src/Environment.java \
--- a/src/Tools/Setup/src/Build.java Sat Jul 24 15:38:41 2021 +0200
+++ b/src/Tools/Setup/src/Build.java Sat Jul 24 16:40:10 2021 +0200
@@ -50,6 +50,8 @@
public static String BUILD_PROPS = "build.props";
public static String COMPONENT_BUILD_PROPS = "etc/build.props";
+ public static String MODULE = "module";
+ public static String NO_BUILD = "no_build";
public static Context component_context(Path dir)
throws IOException
@@ -106,21 +108,27 @@
}
}
+ public boolean get_bool(String name) {
+ String prop = _props.getProperty(name, "false");
+ switch(prop) {
+ case "true": return true;
+ case "false": return false;
+ default:
+ throw new RuntimeException(
+ error_message("Bad boolean property " + Library.quote(name) + ": " + Library.quote(prop)));
+ }
+ }
+
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 module_name() { return _props.getProperty(MODULE, ""); }
+ public String module_result() { return get_bool(NO_BUILD) ? "" : module_name(); }
+
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", ""); }
@@ -421,7 +429,7 @@
{
List<Path> result = new LinkedList<Path>();
for (Context context : component_contexts()) {
- String module = context.module();
+ String module = context.module_result();
if (!module.isEmpty()) { result.add(context.path(module)); }
}
return List.copyOf(result);
@@ -445,7 +453,7 @@
public static void build(Context context, boolean fresh)
throws IOException, InterruptedException, NoSuchAlgorithmException
{
- String module = context.module();
+ String module = context.module_result();
if (!module.isEmpty()) {
String title = context.title();