# HG changeset patch
# User wenzelm
# Date 1627124988 -7200
# Node ID 0ee44ed80290b618dd573bb22ba6b8ab4b726847
# Parent  9ce319c846d9a05adb1db37a0d84e037952c5563
clarified signature;

diff -r 9ce319c846d9 -r 0ee44ed80290 etc/build.props
--- a/etc/build.props	Sat Jul 24 12:24:56 2021 +0200
+++ b/etc/build.props	Sat Jul 24 13:09:48 2021 +0200
@@ -176,6 +176,7 @@
   src/Pure/Tools/phabricator.scala \
   src/Pure/Tools/print_operation.scala \
   src/Pure/Tools/profiling_report.scala \
+  src/Pure/Tools/scala_build.scala \
   src/Pure/Tools/scala_project.scala \
   src/Pure/Tools/server.scala \
   src/Pure/Tools/server_commands.scala \
diff -r 9ce319c846d9 -r 0ee44ed80290 src/Pure/Tools/scala_build.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/scala_build.scala	Sat Jul 24 13:09:48 2021 +0200
@@ -0,0 +1,47 @@
+/*  Title:      Pure/Tools/scala_build.scala
+    Author:     Makarius
+
+Manage and build Isabelle/Scala/Java components.
+*/
+
+package isabelle
+
+
+import java.util.{Properties => JProperties}
+import java.nio.file.Files
+
+import scala.jdk.CollectionConverters._
+
+
+object Scala_Build
+{
+  type Context = isabelle.setup.Build.Context
+
+  def context(dir: Path,
+    component: Boolean = false,
+    more_props: Properties.T = Nil): Context =
+  {
+    val props_name =
+      if (component) isabelle.setup.Build.COMPONENT_BUILD_PROPS
+      else isabelle.setup.Build.BUILD_PROPS
+    val props_path = dir + Path.explode(props_name)
+
+    val props = new JProperties
+    props.load(Files.newBufferedReader(props_path.java_path))
+    for ((a, b) <- more_props) props.put(a, b)
+
+    new isabelle.setup.Build.Context(dir.java_path, props, props_path.implode)
+  }
+
+  def build(dir: Path,
+    fresh: Boolean = false,
+    component: Boolean = false,
+    more_props: Properties.T = Nil): Unit =
+  {
+    isabelle.setup.Build.build(
+      context(dir, component = component, more_props = more_props), fresh)
+  }
+
+  def component_contexts(): List[Context] =
+    isabelle.setup.Build.component_contexts().asScala.toList
+}
diff -r 9ce319c846d9 -r 0ee44ed80290 src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala	Sat Jul 24 12:24:56 2021 +0200
+++ b/src/Pure/Tools/scala_project.scala	Sat Jul 24 13:09:48 2021 +0200
@@ -26,18 +26,13 @@
 
   /* file and directories */
 
-  def plugin_contexts(): List[isabelle.setup.Build.Context] =
+  def plugin_contexts(): List[Scala_Build.Context] =
     for (plugin <- List("jedit_base", "jedit_main"))
-    yield {
-      val dir = Path.explode("$ISABELLE_HOME/src/Tools/jEdit") + Path.basic(plugin)
-      isabelle.setup.Build.directory_context(dir.java_path)
-    }
+    yield Scala_Build.context(Path.explode("$ISABELLE_HOME/src/Tools/jEdit") + Path.basic(plugin))
 
   lazy val isabelle_files: (List[Path], List[Path]) =
   {
-    val contexts =
-      isabelle.setup.Build.component_contexts().asScala.toList :::
-        plugin_contexts()
+    val contexts = Scala_Build.component_contexts() ::: plugin_contexts()
 
     val jars1 = Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH"))
     val jars2 =
@@ -67,7 +62,7 @@
 
   lazy val isabelle_scala_files: Map[String, Path] =
   {
-    val context = isabelle.setup.Build.component_context(Path.ISABELLE_HOME.java_path)
+    val context = Scala_Build.context(Path.ISABELLE_HOME, component = true)
     context.sources().asScala.iterator.foldLeft(Map.empty[String, Path]) {
       case (map, name) =>
         if (name.endsWith(".scala")) {
diff -r 9ce319c846d9 -r 0ee44ed80290 src/Tools/Setup/src/Build.java
--- a/src/Tools/Setup/src/Build.java	Sat Jul 24 12:24:56 2021 +0200
+++ b/src/Tools/Setup/src/Build.java	Sat Jul 24 13:09:48 2021 +0200
@@ -51,21 +51,12 @@
     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)); }
+        props.load(Files.newBufferedReader(props_path));
         return new Context(dir, props, props_path.toString());
     }