clarified settings and defaults;
authorwenzelm
Sun, 09 Dec 2018 12:09:54 +0100
changeset 69434 b93404a4c3dd
parent 69433 9e5938af9ac0
child 69435 e18e4532fb42
clarified settings and defaults;
etc/settings
lib/Tools/components
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_release.scala
src/Pure/Admin/components.scala
src/Pure/Admin/other_isabelle.scala
--- a/etc/settings	Sun Dec 09 00:08:59 2018 +0100
+++ b/etc/settings	Sun Dec 09 12:09:54 2018 +0100
@@ -68,6 +68,7 @@
 ###
 
 ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components"
+ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib"
 
 # The place for user configuration, heap files, etc.
 if [ -z "$ISABELLE_IDENTIFIER" ]; then
--- a/lib/Tools/components	Sun Dec 09 00:08:59 2018 +0100
+++ b/lib/Tools/components	Sun Dec 09 12:09:54 2018 +0100
@@ -87,7 +87,7 @@
 
 if [ -n "$INIT_SETTINGS" ]; then
   SETTINGS="$ISABELLE_HOME_USER/etc/settings"
-  SETTINGS_CONTENT='init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"'
+  SETTINGS_CONTENT='init_components "$ISABELLE_COMPONENTS_BASE" "$ISABELLE_HOME/Admin/components/main"'
   if [ -e "$SETTINGS" ]; then
     echo "User settings file already exists!"
     echo
--- a/src/Pure/Admin/build_history.scala	Sun Dec 09 00:08:59 2018 +0100
+++ b/src/Pure/Admin/build_history.scala	Sun Dec 09 12:09:54 2018 +0100
@@ -112,7 +112,7 @@
     afp_partition: Int = 0,
     isabelle_identifier: String = default_isabelle_identifier,
     ml_statistics_step: Int = 1,
-    components_base: Option[Path] = None,
+    components_base: Path = Components.default_components_base,
     fresh: Boolean = false,
     hostname: String = "",
     multicore_base: Boolean = false,
@@ -186,7 +186,8 @@
       /* init settings */
 
       val component_settings =
-        other_isabelle.init_components(base = components_base, catalogs = List("main", "optional"))
+        other_isabelle.init_components(
+          components_base = components_base, catalogs = List("main", "optional"))
       other_isabelle.init_settings(component_settings ::: init_settings)
       other_isabelle.resolve_components(verbose)
       val ml_platform =
@@ -396,7 +397,7 @@
     Command_Line.tool0 {
       var afp_rev: Option[String] = None
       var multicore_base = false
-      var components_base: Option[Path] = None
+      var components_base: Path = Components.default_components_base
       var heap: Option[Int] = None
       var max_heap: Option[Int] = None
       var multicore_list = List(default_multicore)
@@ -421,7 +422,8 @@
   Options are:
     -A REV       include $ISABELLE_HOME/AFP repository at given revision
     -B           first multicore build serves as base for scheduling information
-    -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
+    -C DIR       base directory for Isabelle components (default: """ +
+      Components.default_components_base + """)
     -H SIZE      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ +
       default_heap * 2 + """ for x86_64)
     -M MULTICORE multicore configurations (see below)
@@ -449,7 +451,7 @@
 """,
         "A:" -> (arg => afp_rev = Some(arg)),
         "B" -> (_ => multicore_base = true),
-        "C:" -> (arg => components_base = Some(Path.explode(arg))),
+        "C:" -> (arg => components_base = 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),
--- a/src/Pure/Admin/build_release.scala	Sun Dec 09 00:08:59 2018 +0100
+++ b/src/Pure/Admin/build_release.scala	Sun Dec 09 12:09:54 2018 +0100
@@ -224,7 +224,7 @@
 
   def build_release(base_dir: Path,
     options: Options,
-    components_base: Option[Path] = None,
+    components_base: Path = Components.default_components_base,
     progress: Progress = No_Progress,
     rev: String = "",
     afp_rev: String = "",
@@ -316,7 +316,7 @@
       val other_isabelle = release.other_isabelle(release.dist_dir)
 
       other_isabelle.init_settings(
-        other_isabelle.init_components(base = components_base, catalogs = List("main")))
+        other_isabelle.init_components(components_base = components_base, catalogs = List("main")))
       other_isabelle.resolve_components(echo = true)
 
       try {
@@ -414,8 +414,8 @@
           val (bundled_components, jdk_component) =
             get_bundled_components(isabelle_target, platform)
 
-          Components.resolve(other_isabelle.components_base(components_base),
-            bundled_components, target_dir = Some(contrib_dir), progress = progress)
+          Components.resolve(components_base, bundled_components,
+            target_dir = Some(contrib_dir), progress = progress)
 
           val more_components_names =
             more_components.map(Components.unpack(contrib_dir, _, progress = progress))
@@ -709,7 +709,7 @@
   {
     Command_Line.tool0 {
       var afp_rev = ""
-      var components_base: Option[Path] = None
+      var components_base: Path = Components.default_components_base
       var official_release = false
       var proper_release_name: Option[String] = None
       var website: Option[Path] = None
@@ -725,7 +725,8 @@
 
   Options are:
     -A REV       corresponding AFP changeset id
-    -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
+    -C DIR       base directory for Isabelle components (default: """ +
+        Components.default_components_base + """)
     -O           official release (not release-candidate)
     -R RELEASE   proper release with name
     -W WEBSITE   produce minimal website in given directory
@@ -739,7 +740,7 @@
   Build Isabelle release in base directory, using the local repository clone.
 """,
         "A:" -> (arg => afp_rev = arg),
-        "C:" -> (arg => components_base = Some(Path.explode(arg))),
+        "C:" -> (arg => components_base = Path.explode(arg)),
         "O" -> (_ => official_release = true),
         "R:" -> (arg => proper_release_name = Some(arg)),
         "W:" -> (arg => website = Some(Path.explode(arg))),
--- a/src/Pure/Admin/components.scala	Sun Dec 09 00:08:59 2018 +0100
+++ b/src/Pure/Admin/components.scala	Sun Dec 09 12:09:54 2018 +0100
@@ -38,6 +38,8 @@
 
   /* component collections */
 
+  val default_components_base = Path.explode("$ISABELLE_COMPONENTS_BASE")
+
   def admin(dir: Path): Path = dir + Path.explode("Admin/components")
 
   def contrib(dir: Path = Path.current, name: String = ""): Path =
--- a/src/Pure/Admin/other_isabelle.scala	Sun Dec 09 00:08:59 2018 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Sun Dec 09 12:09:54 2018 +0100
@@ -68,20 +68,17 @@
 
   /* components */
 
-  def components_base(base: Option[Path]): Path =
-    base getOrElse Components.contrib(isabelle_home_user.dir)
-
   def init_components(
-    base: Option[Path] = None,
+    components_base: Path = Components.default_components_base,
     catalogs: List[String] = Nil,
     components: List[String] = Nil): List[String] =
   {
-    val base_dir = components_base(base)
     val dir = Components.admin(isabelle_home)
     catalogs.map(name =>
-      "init_components " + File.bash_path(base_dir) + " " + File.bash_path(dir + Path.basic(name))) :::
+      "init_components " + File.bash_path(components_base) + " " +
+        File.bash_path(dir + Path.basic(name))) :::
     components.map(name =>
-      "init_component " + File.bash_path(base_dir + Path.basic(name)))
+      "init_component " + File.bash_path(components_base + Path.basic(name)))
   }