# HG changeset patch
# User wenzelm
# Date 1627137610 -7200
# Node ID 22ad3ac2152c134465726acbab1a88037408c2d8
# Parent  fb8d5c0133c98ac2ed9301e517adeb43ece97a86
clarified properties: "module" and "no_build";
clarified signature;

diff -r fb8d5c0133c9 -r 22ad3ac2152c Admin/components/components.sha1
--- 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
diff -r fb8d5c0133c9 -r 22ad3ac2152c Admin/components/main
--- 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
diff -r fb8d5c0133c9 -r 22ad3ac2152c src/Doc/System/Scala.thy
--- 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
diff -r fb8d5c0133c9 -r 22ad3ac2152c src/Pure/Admin/build_jedit.scala
--- 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"))
     })
diff -r fb8d5c0133c9 -r 22ad3ac2152c src/Pure/Tools/scala_build.scala
--- 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] =
diff -r fb8d5c0133c9 -r 22ad3ac2152c src/Tools/Setup/etc/build.props
--- 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 \
diff -r fb8d5c0133c9 -r 22ad3ac2152c src/Tools/Setup/src/Build.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();