# HG changeset patch
# User wenzelm
# Date 1543762574 -3600
# Node ID fc58534bc475403ed4e04beb061b7b259f98efa0
# Parent  ff9095c91e87fdf416f6386f873aff4bfc6e0400
clarified component settings;

diff -r ff9095c91e87 -r fc58534bc475 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sun Dec 02 14:12:08 2018 +0100
+++ b/src/Pure/Admin/build_history.scala	Sun Dec 02 15:56:14 2018 +0100
@@ -112,7 +112,7 @@
     afp_partition: Int = 0,
     isabelle_identifier: String = default_isabelle_identifier,
     ml_statistics_step: Int = 1,
-    components_base: String = "",
+    components_base: Option[Path] = None,
     fresh: Boolean = false,
     hostname: String = "",
     multicore_base: Boolean = false,
@@ -185,7 +185,11 @@
     {
       /* init settings */
 
-      other_isabelle.init_settings(components_base, init_settings)
+      val component_settings =
+        other_isabelle.init_components(
+          base = components_base getOrElse other_isabelle.default_components_base,
+          catalogs = List("main", "optional"))
+      other_isabelle.init_settings(component_settings ::: init_settings)
       other_isabelle.resolve_components(verbose)
       val ml_platform =
         augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
@@ -394,7 +398,7 @@
     Command_Line.tool0 {
       var afp_rev: Option[String] = None
       var multicore_base = false
-      var components_base = ""
+      var components_base: Option[Path] = None
       var heap: Option[Int] = None
       var max_heap: Option[Int] = None
       var multicore_list = List(default_multicore)
@@ -447,7 +451,7 @@
 """,
         "A:" -> (arg => afp_rev = Some(arg)),
         "B" -> (_ => multicore_base = true),
-        "C:" -> (arg => components_base = arg),
+        "C:" -> (arg => components_base = Some(Path.explode(arg))),
         "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
         "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse(_))),
         "N:" -> (arg => isabelle_identifier = arg),
diff -r ff9095c91e87 -r fc58534bc475 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Sun Dec 02 14:12:08 2018 +0100
+++ b/src/Pure/Admin/build_release.scala	Sun Dec 02 15:56:14 2018 +0100
@@ -246,7 +246,8 @@
           isabelle_identifier = release.other_isabelle_identifier,
           progress = progress)
 
-      other_isabelle.init_settings((base_dir.absolute + Path.explode("contrib")).implode, Nil)
+      other_isabelle.init_settings(
+        other_isabelle.init_components(base = base_dir.absolute + Path.explode("contrib")))
       other_isabelle.resolve_components(echo = true)
 
       try {
diff -r ff9095c91e87 -r fc58534bc475 src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Sun Dec 02 14:12:08 2018 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Sun Dec 02 15:56:14 2018 +0100
@@ -24,7 +24,7 @@
 {
   other_isabelle =>
 
-  override def toString: String = isabelle_home.toString
+  override def toString: String = isabelle_home.absolute.toString
 
   if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined)
     error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
@@ -66,6 +66,22 @@
       foreach(entry => File.copy(entry.path, target_dir))
 
 
+  /* components */
+
+  def default_components_base: Path = isabelle_home_user.absolute.dir + Path.explode("contrib")
+  def default_components_dir: Path = isabelle_home.absolute + Path.explode("Admin/components")
+  def default_catalogs: List[String] = List("main")
+
+  def init_components(
+    base: Path = default_components_base,
+    dir: Path = default_components_dir,
+    catalogs: List[String] = default_catalogs): List[String] =
+  {
+    catalogs.map(catalog =>
+      "init_components " + File.bash_path(base) + " " + File.bash_path(dir + Path.basic(catalog)))
+  }
+
+
   /* settings */
 
   def clean_settings(): Boolean =
@@ -75,7 +91,7 @@
     }
     else false
 
-  def init_settings(components_base: String, more_settings: List[String])
+  def init_settings(settings: List[String])
   {
     if (!clean_settings())
       error("Cannot proceed with existing user settings file: " + etc_settings)
@@ -83,25 +99,8 @@
     Isabelle_System.mkdirs(etc_settings.dir)
     File.write(etc_settings,
       "# generated by Isabelle " + Date.now() + "\n" +
-      "#-*- shell-script -*- :mode=shellscript:\n")
-
-    val component_settings =
-    {
-      val components_base_path =
-        if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
-        else Path.explode(components_base).expand
-
-      val catalogs = List("main", "optional")
-      catalogs.map(catalog =>
-        "init_components " + File.bash_path(components_base_path) +
-          " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
-    }
-
-    val settings =
-      List(component_settings) :::
-      (if (more_settings.isEmpty) Nil else List(more_settings))
-
-    File.append(etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
+      "#-*- shell-script -*- :mode=shellscript:\n" +
+      settings.mkString("\n", "\n", "\n"))
   }