# HG changeset patch
# User wenzelm
# Date 1674597932 -3600
# Node ID 6e2c6ccc5dc02e6d62b7463b96a61381a3a4c7f8
# Parent  7770537f5ceb706e499aeab05fb6d31b06c9222c
clarified defaults: imitate "isabelle components -I" without further parameters;

diff -r 7770537f5ceb -r 6e2c6ccc5dc0 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Jan 24 22:48:28 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Tue Jan 24 23:05:32 2023 +0100
@@ -186,7 +186,6 @@
       val component_settings =
         other_isabelle.init_components(
           component_repository = component_repository,
-          components_base = Components.standard_components_base,
           catalogs = Components.optional_catalogs)
       other_isabelle.init_settings(component_settings ::: init_settings)
       other_isabelle.resolve_components(echo = verbose)
diff -r 7770537f5ceb -r 6e2c6ccc5dc0 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Tue Jan 24 22:48:28 2023 +0100
+++ b/src/Pure/Admin/build_release.scala	Tue Jan 24 23:05:32 2023 +0100
@@ -23,13 +23,12 @@
     def apply(
       target_dir: Path,
       release_name: String = "",
-      components_base: Path = Components.default_components_base,
       progress: Progress = new Progress
     ): Release_Context = {
       val date = Date.now()
       val dist_name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date))
       val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute
-      new Release_Context(release_name, dist_name, dist_dir, components_base, progress)
+      new Release_Context(release_name, dist_name, dist_dir, progress)
     }
   }
 
@@ -37,7 +36,6 @@
     val release_name: String,
     val dist_name: String,
     val dist_dir: Path,
-    val components_base: Path,
     val progress: Progress
   ) {
     override def toString: String = dist_name
@@ -466,8 +464,7 @@
 
       val other_isabelle = context.other_isabelle(context.dist_dir)
 
-      other_isabelle.init_settings(
-        other_isabelle.init_components(components_base = context.components_base))
+      other_isabelle.init_settings(other_isabelle.init_components())
       other_isabelle.resolve_components(echo = true)
 
       other_isabelle.scala_build(echo = true)
@@ -561,7 +558,7 @@
           get_bundled_components(isabelle_target, platform)
 
         for (name <- bundled_components) {
-          Components.resolve(context.components_base, name,
+          Components.resolve(Components.default_components_base, name,
             target_dir = Some(contrib_dir),
             copy_dir = Some(context.dist_dir + Path.explode("contrib")),
             progress = progress)
@@ -874,7 +871,6 @@
   def main(args: Array[String]): Unit = {
     Command_Line.tool {
       var afp_rev = ""
-      var components_base: Path = Components.default_components_base
       var target_dir = Path.current
       var release_name = ""
       var source_archive = ""
@@ -892,8 +888,6 @@
 
   Options are:
     -A REV       corresponding AFP changeset id
-    -C DIR       base directory for Isabelle components (default: """ +
-        Components.default_components_base + """)
     -D DIR       target directory (default ".")
     -R RELEASE   explicit release name
     -S ARCHIVE   use existing source archive (file or URL)
@@ -909,7 +903,6 @@
   Build Isabelle release in base directory, using the local repository clone.
 """,
         "A:" -> (arg => afp_rev = arg),
-        "C:" -> (arg => components_base = Path.explode(arg)),
         "D:" -> (arg => target_dir = Path.explode(arg)),
         "R:" -> (arg => release_name = arg),
         "S:" -> (arg => source_archive = arg),
@@ -935,10 +928,7 @@
 
       val progress = new Console_Progress()
       def make_context(name: String): Release_Context =
-        Release_Context(target_dir,
-          release_name = name,
-          components_base = components_base,
-          progress = progress)
+        Release_Context(target_dir, release_name = name, progress = progress)
 
       val context =
         if (source_archive.isEmpty) {
diff -r 7770537f5ceb -r 6e2c6ccc5dc0 src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Tue Jan 24 22:48:28 2023 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Tue Jan 24 23:05:32 2023 +0100
@@ -89,18 +89,15 @@
 
   def init_components(
     component_repository: String = Components.default_component_repository,
-    components_base: Path = Components.default_components_base,
     catalogs: List[String] = Components.default_catalogs,
     components: List[String] = Nil
   ): List[String] = {
-    val dir = Components.admin(isabelle_home)
+    val admin = Components.admin(Path.ISABELLE_HOME).implode
+    val components_base = quote("${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}")
 
     ("ISABELLE_COMPONENT_REPOSITORY=" + Bash.string(component_repository)) ::
-    catalogs.map(name =>
-      "init_components " + File.bash_path(components_base) + " " +
-        File.bash_path(dir + Path.basic(name))) :::
-    components.map(name =>
-      "init_component " + File.bash_path(components_base + Path.basic(name)))
+    catalogs.map(name => "init_components " + components_base + " " + quote(admin + "/" + name)) :::
+    components.map(name => "init_component " + components_base + "/" + name)
   }
 
 
diff -r 7770537f5ceb -r 6e2c6ccc5dc0 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Tue Jan 24 22:48:28 2023 +0100
+++ b/src/Pure/System/components.scala	Tue Jan 24 23:05:32 2023 +0100
@@ -39,7 +39,6 @@
     Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY")
 
   val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
-  val standard_components_base: Path = Path.explode("$USER_HOME/.isabelle/contrib")
 
   val default_catalogs: List[String] = List("main")
   val optional_catalogs: List[String] = List("main", "optional")