diff --git a/etc/settings b/etc/settings
--- a/etc/settings
+++ b/etc/settings
@@ -1,169 +1,170 @@
 # -*- shell-script -*- :mode=shellscript:
 #
 # Isabelle system settings.
 #
 # Important notes:
 #   * See the "system" manual for explanations on Isabelle settings
 #   * User settings go into $ISABELLE_HOME_USER/etc/settings
 #   * DO NOT EDIT the repository copy of this file!
 #   * DO NOT COPY this file into the $ISABELLE_HOME_USER directory!
 
 ###
 ### Isabelle/Scala
 ###
 
 ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms128m -J-Xmx1024m -J-Xss2m"
 
 ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0 -Djdk.gtk.version=2.2 --illegal-access=warn"
 
 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss16m"
 
 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
 
 isabelle_scala_tools 'isabelle.Regular_Tools'
 [ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_tools 'isabelle.Admin_Tools'
 
 isabelle_file_format 'isabelle.Bibtex$File_Format'
 
 #paranoia settings -- avoid intrusion of alien options
 unset "_JAVA_OPTIONS"
 unset "JAVA_TOOL_OPTIONS"
 
 #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc.
 unset XMODIFIERS
 
 
 ###
 ### Interactive sessions (cf. isabelle console)
 ###
 
 ISABELLE_LINE_EDITOR="rlwrap"
 
 
 ###
 ### Batch sessions (cf. isabelle build)
 ###
 
 ISABELLE_BUILD_OPTIONS=""
 
 
 ###
 ### Document preparation (cf. isabelle latex/document)
 ###
 
 ISABELLE_LATEX="latex -file-line-error"
 ISABELLE_PDFLATEX="pdflatex -file-line-error"
 ISABELLE_BIBTEX="bibtex"
 ISABELLE_MAKEINDEX="makeindex"
 ISABELLE_EPSTOPDF="epstopdf"
 
 if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
   ISABELLE_LATEX="latex -c-style-errors"
   ISABELLE_PDFLATEX="pdflatex -c-style-errors"
 fi
 
 
 ###
 ### Misc path settings
 ###
 
 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
   ISABELLE_HOME_USER="$USER_HOME/.isabelle"
 else
   ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"
 fi
 
 # Where to look for isabelle tools (multiple dirs separated by ':').
 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
 
 # Location for temporary files (should be on a local file system).
 ISABELLE_TMP_PREFIX="${TMPDIR:-/tmp}/isabelle-$USER"
 
 # Heap locations.
 ISABELLE_HEAPS="$ISABELLE_HOME_USER/heaps"
 ISABELLE_HEAPS_SYSTEM="$ISABELLE_HOME/heaps"
 
 # HTML browser info.
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info"
 
 # Site settings check -- just to make it a little bit harder to copy this file verbatim!
 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
   { echo >&2 "### Isabelle site settings already present!  Maybe copied etc/settings in full?"; }
 ISABELLE_SITE_SETTINGS_PRESENT=true
 
 
 ###
 ### Default logic
 ###
 
 ISABELLE_LOGIC=HOL
 
 
 ###
 ### Docs
 ###
 
 # Where to look for docs (multiple dirs separated by ':').
 ISABELLE_DOCS="$ISABELLE_HOME/doc"
 
 ISABELLE_DOCS_RELEASE_NOTES="~~/ANNOUNCE:~~/README:~~/NEWS:~~/COPYRIGHT:~~/CONTRIBUTORS:~~/contrib/README:~~/src/Tools/jEdit/README:~~/README_REPOSITORY"
 ISABELLE_DOCS_EXAMPLES="~~/src/HOL/ex/Seq.thy:~~/src/HOL/ex/ML.thy:~~/src/HOL/Unix/Unix.thy:~~/src/HOL/Isar_Examples/Drinker.thy:~~/src/Tools/SML/Examples.thy:~~/src/Pure/ROOT.ML"
 
 # "open" within desktop environment (potentially asynchronous)
 case "$ISABELLE_PLATFORM_FAMILY" in
   linux)
     ISABELLE_OPEN="xdg-open"
     ;;
   macos)
     ISABELLE_OPEN="open"
     ;;
   windows)
     ISABELLE_OPEN="cygstart"
     ;;
 esac
 
 PDF_VIEWER="$ISABELLE_OPEN"
 DVI_VIEWER="$ISABELLE_OPEN"
 
 
 ###
 ### Symbol rendering
 ###
 
 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
 
 
 ###
 ### OCaml
 ###
 
 ISABELLE_OPAM_ROOT="$ISABELLE_HOME_USER/opam"
 
 ISABELLE_OCAML_VERSION="4.05.0"
 
 
 ###
 ### Haskell
 ###
 
 ISABELLE_STACK_ROOT="$ISABELLE_HOME_USER/stack"
 
 ISABELLE_STACK_RESOLVER="lts-12.13"
 
 ISABELLE_GHC_VERSION="ghc-8.4.3"
 
 
 ###
 ### Misc settings
 ###
 
 ISABELLE_GNUPLOT="gnuplot"
 ISABELLE_FONTFORGE="fontforge"
 
 #ISABELLE_MLTON="/usr/bin/mlton"
 #ISABELLE_SMLNJ="/usr/bin/sml"
 #ISABELLE_SWIPL="/usr/bin/swipl"
diff --git a/lib/Tools/components b/lib/Tools/components
--- a/lib/Tools/components
+++ b/lib/Tools/components
@@ -1,146 +1,146 @@
 #!/usr/bin/env bash
 #
 # Author: Makarius
 #
 # DESCRIPTION: resolve Isabelle components
 
 
 ## diagnostics
 
 PRG="$(basename "$0")"
 
 function usage()
 {
   echo
   echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]"
   echo
   echo "  Options are:"
   echo "    -I           init user settings"
   echo "    -R URL       component repository (default \$ISABELLE_COMPONENT_REPOSITORY)"
   echo "    -a           resolve all missing components"
   echo "    -l           list status"
   echo
   echo "  Resolve Isabelle components via download and installation."
   echo "  COMPONENTS are identified via base name."
   echo
   echo "  ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
   echo
   exit 1
 }
 
 function fail()
 {
   echo "$1" >&2
   exit 2
 }
 
 
 ## process command line
 
 #options
 
 INIT_SETTINGS=""
 COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
 ALL_MISSING=""
 LIST_ONLY=""
 
 while getopts "IR:al" OPT
 do
   case "$OPT" in
     I)
       INIT_SETTINGS="true"
       ;;
     R)
       COMPONENT_REPOSITORY="$OPTARG"
       ;;
     a)
       ALL_MISSING="true"
       ;;
     l)
       LIST_ONLY="true"
       ;;
     \?)
       usage
       ;;
   esac
 done
 
 shift $(($OPTIND - 1))
 
 
 # args
 
 [ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage
 
 if [ -z "$ALL_MISSING" ]; then
   splitarray ":" "$@"
 else
   splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"
 fi
 declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")
 
 
 ## main
 
 splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")
 splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")
 
 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
     echo "Edit \"$SETTINGS\" manually"
     echo "and add the following line near its start:"
     echo
     echo "  $SETTINGS_CONTENT"
     echo
   else
     echo "Initializing \"$SETTINGS\""
     mkdir -p "$(dirname "$SETTINGS")"
     echo "$SETTINGS_CONTENT" > "$SETTINGS"
   fi
 elif [ -n "$LIST_ONLY" ]; then
   echo
   echo "Available components:"
   for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo "  $NAME"; done
   echo
   echo "Missing components:"
   for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done
 else
   for NAME in "${SELECTED_COMPONENTS[@]}"
   do
     BASE_NAME="$(basename "$NAME")"
     FULL_NAME=""
     for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"
     do
       [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"
     done
     if [ -z "$FULL_NAME" ]; then
       echo "Ignoring irrelevant component \"$NAME\""
     elif [ -d "$FULL_NAME" ]; then
       echo "Skipping existing component \"$FULL_NAME\""
     else
       if [ ! -e "${FULL_NAME}.tar.gz" ]; then
         REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
         type -p curl > /dev/null || fail "Cannot download files: missing curl"
         echo "Getting \"$REMOTE\""
         mkdir -p "$(dirname "$FULL_NAME")"
         curl --fail --silent "$REMOTE" > "${FULL_NAME}.tar.gz.part" || \
           fail "Failed to download \"$REMOTE\""
         if perl -e "exit((stat('${FULL_NAME}.tar.gz.part'))[7] == 0 ? 0 : 1);"
         then
           rm -f "${FULL_NAME}.tar.gz.part"
         else
           mv "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
         fi
       fi
       if [ -e "${FULL_NAME}.tar.gz" ]; then
         echo "Unpacking \"${FULL_NAME}.tar.gz\""
         tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2
       fi
     fi
   done
 fi
 
diff --git a/src/Pure/Admin/build_history.scala b/src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala
+++ b/src/Pure/Admin/build_history.scala
@@ -1,592 +1,594 @@
 /*  Title:      Pure/Admin/build_history.scala
     Author:     Makarius
 
 Build other history versions.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 import java.time.format.DateTimeFormatter
 import java.util.Locale
 
 
 object Build_History
 {
   /* log files */
 
   val engine = "build_history"
   val log_prefix = engine + "_"
   val META_INFO_MARKER = "\fmeta_info = "
 
 
   /* augment settings */
 
   def augment_settings(
     other_isabelle: Other_Isabelle,
     threads: Int,
     arch_64: Boolean,
     heap: Int,
     max_heap: Option[Int],
     more_settings: List[String]): String =
   {
     val (ml_platform, ml_settings) =
     {
       val windows_32 = "x86-windows"
       val windows_64 = "x86_64-windows"
       val platform_32 = other_isabelle.getenv("ISABELLE_PLATFORM32")
       val platform_64 = other_isabelle.getenv("ISABELLE_PLATFORM64")
       val platform_family = other_isabelle.getenv("ISABELLE_PLATFORM_FAMILY")
 
       val polyml_home =
         try { Path.explode(other_isabelle.getenv("ML_HOME")).dir }
         catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
 
       def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
 
       def err(platform: String): Nothing =
         error("Platform " + platform + " unavailable on this machine")
 
       def check_dir(platform: String): Boolean =
         platform != "" && ml_home(platform).is_dir
 
       val ml_platform =
         if (Platform.is_windows && arch_64) {
           if (check_dir(windows_64)) windows_64 else err(windows_64)
         }
         else if (Platform.is_windows && !arch_64) {
           if (check_dir(windows_32)) windows_32
           else platform_32  // x86-cygwin
         }
         else {
           val (platform, platform_name) =
             if (arch_64) (platform_64, "x86_64-" + platform_family)
             else (platform_32, "x86-" + platform_family)
           if (check_dir(platform)) platform else err(platform_name)
         }
 
       val ml_options =
         "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
         " --gcthreads " + threads +
         (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
 
       (ml_platform,
         List(
           "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
           "ML_PLATFORM=" + quote(ml_platform),
           "ML_OPTIONS=" + quote(ml_options)))
     }
 
     val thread_settings =
       List(
         "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
         "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
 
     val settings =
       List(ml_settings, thread_settings) :::
       (if (more_settings.isEmpty) Nil else List(more_settings))
 
     File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
 
     ml_platform
   }
 
 
 
   /** build_history **/
 
   private val default_user_home = Path.explode("$USER_HOME")
   private val default_rev = "tip"
   private val default_multicore = (1, 1)
   private val default_heap = 1500
   private val default_isabelle_identifier = "build_history"
 
   def build_history(
     options: Options,
     root: Path,
     user_home: Path = default_user_home,
     progress: Progress = No_Progress,
     rev: String = default_rev,
     afp_rev: Option[String] = None,
     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,
     multicore_list: List[(Int, Int)] = List(default_multicore),
     arch_64: Boolean = false,
     heap: Int = default_heap,
     max_heap: Option[Int] = None,
     init_settings: List[String] = Nil,
     more_settings: List[String] = Nil,
     verbose: Boolean = false,
     build_tags: List[String] = Nil,
     build_args: List[String] = Nil): List[(Process_Result, Path)] =
   {
     /* sanity checks */
 
     if (File.eq(Path.explode("~~"), root))
       error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
 
     for ((threads, _) <- multicore_list if threads < 1)
       error("Bad threads value < 1: " + threads)
     for ((_, processes) <- multicore_list if processes < 1)
       error("Bad processes value < 1: " + processes)
 
     if (heap < 100) error("Bad heap value < 100: " + heap)
 
     if (max_heap.isDefined && max_heap.get < heap)
       error("Bad max_heap value < heap: " + max_heap.get)
 
     System.getenv("ISABELLE_SETTINGS_PRESENT") match {
       case null | "" =>
       case _ => error("Cannot run build_history within existing Isabelle settings environment")
     }
 
 
     /* checkout Isabelle + AFP repository */
 
     def checkout(dir: Path, version: String): String =
     {
       val hg = Mercurial.repository(dir)
       hg.update(rev = version, clean = true)
       progress.echo_if(verbose, hg.log(version, options = "-l1"))
       hg.id(rev = version)
     }
 
     val isabelle_version = checkout(root, rev)
 
     val afp_repos = root + Path.explode("AFP")
     val afp_version = afp_rev.map(checkout(afp_repos, _))
 
     val (afp_build_args, afp_sessions) =
       if (afp_rev.isEmpty) (Nil, Nil)
       else {
         val afp = AFP.init(options, afp_repos)
         (List("-d", "~~/AFP/thys"), afp.partition(afp_partition))
       }
 
 
     /* main */
 
     val other_isabelle =
       Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
         user_home = user_home, progress = progress)
 
     val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname()
     val build_history_date = Date.now()
     val build_group_id = build_host + ":" + build_history_date.time.ms
 
     var first_build = true
     for ((threads, processes) <- multicore_list) yield
     {
       /* 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 =
         augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
 
       val isabelle_output =
         other_isabelle.isabelle_home_user + Path.explode("heaps") +
           Path.explode(other_isabelle.getenv("ML_IDENTIFIER"))
       val isabelle_output_log = isabelle_output + Path.explode("log")
       val isabelle_base_log = isabelle_output + Path.explode("../base_log")
 
       if (first_build) {
         other_isabelle.resolve_components(verbose)
 
         if (fresh)
           Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
         other_isabelle.bash(
           "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
             "bin/isabelle jedit -b", redirect = true, echo = verbose).check
 
         for {
           tool <- List("ghc_setup", "ocaml_setup")
           if other_isabelle.getenv("ISABELLE_" + Word.uppercase(tool)) == "true" &&
             (other_isabelle.isabelle_home + Path.explode("lib/Tools/" + tool)).is_file
         } other_isabelle(tool, echo = verbose)
 
         Isabelle_System.rm_tree(isabelle_base_log)
       }
 
       Isabelle_System.rm_tree(isabelle_output)
       Isabelle_System.mkdirs(isabelle_output)
 
       val log_path =
         other_isabelle.isabelle_home_user +
           Build_Log.log_subdir(build_history_date) +
           Build_Log.log_filename(Build_History.engine, build_history_date,
             List(build_host, ml_platform, "M" + threads) ::: build_tags)
 
       Isabelle_System.mkdirs(log_path.dir)
 
       val build_out = other_isabelle.isabelle_home_user + Path.explode("log/build.out")
       val build_out_progress = new File_Progress(build_out)
       build_out.file.delete
 
 
       /* build */
 
       if (multicore_base && !first_build && isabelle_base_log.is_dir)
         Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
 
       val build_start = Date.now()
       val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
       val build_result =
         Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
           user_home = user_home, progress = build_out_progress)(
             "build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true,
             strict = false)
       val build_end = Date.now()
 
       val build_info: Build_Log.Build_Info =
         Build_Log.Log_File(log_path.file_name, build_result.out_lines).
           parse_build_info(ml_statistics = true)
 
 
       /* output log */
 
       val store = Sessions.store(options + "build_database_server=false")
 
       val meta_info =
         Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) :::
         Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) :::
         List(
           Build_Log.Prop.build_group_id.name -> build_group_id,
           Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms),
           Build_Log.Prop.build_engine.name -> Build_History.engine,
           Build_Log.Prop.build_host.name -> build_host,
           Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start),
           Build_Log.Prop.build_end.name -> Build_Log.print_date(build_end),
           Build_Log.Prop.isabelle_version.name -> isabelle_version) :::
         afp_version.map(Build_Log.Prop.afp_version.name -> _).toList
 
       build_out_progress.echo("Reading session build info ...")
       val session_build_info =
         build_info.finished_sessions.flatMap(session_name =>
           {
             val database = isabelle_output + store.database(session_name)
 
             if (database.is_file) {
               using(SQLite.open_database(database))(db =>
               {
                 val theory_timings =
                   try {
                     store.read_theory_timings(db, session_name).map(ps =>
                       Build_Log.Log_File.print_props(Build_Log.THEORY_TIMING_MARKER,
                         (Build_Log.SESSION_NAME, session_name) :: ps))
                   }
                   catch { case ERROR(_) => Nil }
 
                 val session_sources =
                   store.read_build(db, session_name).map(_.sources) match {
                     case Some(sources) if sources.length == SHA1.digest_length =>
                       List("Sources " + session_name + " " + sources)
                     case _ => Nil
                   }
 
                 theory_timings ::: session_sources
               })
             }
             else Nil
           })
 
       build_out_progress.echo("Reading ML statistics ...")
       val ml_statistics =
         build_info.finished_sessions.flatMap(session_name =>
           {
             val database = isabelle_output + store.database(session_name)
             val log_gz = isabelle_output + store.log_gz(session_name)
 
             val properties =
               if (database.is_file) {
                 using(SQLite.open_database(database))(db =>
                   store.read_ml_statistics(db, session_name))
               }
               else if (log_gz.is_file) {
                 Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
               }
               else Nil
 
             val trimmed_properties =
               if (ml_statistics_step <= 0) Nil
               else if (ml_statistics_step == 1) properties
               else {
                 (for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 }
                  yield ps).toList
               }
 
             trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps)
           })
 
       build_out_progress.echo("Reading error messages ...")
       val session_errors =
         build_info.failed_sessions.flatMap(session_name =>
           {
             val database = isabelle_output + store.database(session_name)
             val errors =
               if (database.is_file) {
                 try {
                   using(SQLite.open_database(database))(db => store.read_errors(db, session_name))
                 } // column "errors" could be missing
                 catch { case _: java.sql.SQLException => Nil }
               }
               else Nil
             errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg))
           })
 
       build_out_progress.echo("Reading heap sizes ...")
       val heap_sizes =
         build_info.finished_sessions.flatMap(session_name =>
           {
             val heap = isabelle_output + Path.explode(session_name)
             if (heap.is_file)
               Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
             else None
           })
 
       build_out_progress.echo("Writing log file " + log_path.ext("xz") + " ...")
       File.write_xz(log_path.ext("xz"),
         terminate_lines(
           Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: build_result.out_lines :::
           session_build_info :::
           ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
           session_errors.map(Build_Log.Log_File.print_props(Build_Log.ERROR_MESSAGE_MARKER, _)) :::
           heap_sizes), XZ.options(6))
 
 
       /* next build */
 
       if (multicore_base && first_build && isabelle_output_log.is_dir)
         Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log)
 
       Isabelle_System.rm_tree(isabelle_output)
 
       first_build = false
 
       (build_result, log_path.ext("xz"))
     }
   }
 
 
   /* command line entry point */
 
   private object Multicore
   {
     private val Pat1 = """^(\d+)$""".r
     private val Pat2 = """^(\d+)x(\d+)$""".r
 
     def parse(s: String): (Int, Int) =
       s match {
         case Pat1(Value.Int(x)) => (x, 1)
         case Pat2(Value.Int(x), Value.Int(y)) => (x, y)
         case _ => error("Bad multicore configuration: " + quote(s))
       }
   }
 
   def main(args: Array[String])
   {
     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)
       var isabelle_identifier = default_isabelle_identifier
       var afp_partition = 0
       var more_settings: List[String] = Nil
       var fresh = false
       var hostname = ""
       var init_settings: List[String] = Nil
       var arch_64 = false
       var output_file = ""
       var rev = default_rev
       var ml_statistics_step = 1
       var build_tags = List.empty[String]
       var user_home = default_user_home
       var verbose = false
       var exit_code = false
 
       val getopts = Getopts("""
 Usage: Admin/build_history [OPTIONS] REPOSITORY [ARGS ...]
 
   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)
     -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
     -P NUMBER    AFP partition number (0, 1, 2, default: 0=unrestricted)
     -U SIZE      maximal ML heap in MB (default: unbounded)
     -e TEXT      additional text for generated etc/settings
     -f           fresh build of Isabelle/Scala components (recommended)
     -h NAME      override local hostname
     -i TEXT      initial text for generated etc/settings
     -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
     -o FILE      output file for log names (default: stdout)
     -r REV       update to revision (default: """ + default_rev + """)
     -s NUMBER    step size for ML statistics (0=none, 1=all, n=step, default: 1)
     -t TAG       free-form build tag (multiple occurrences possible)
     -u DIR       alternative USER_HOME directory
     -v           verbose
     -x           return overall exit code from build processes
 
   Build Isabelle sessions from the history of another REPOSITORY clone,
   passing ARGS directly to its isabelle build tool.
 
   Each MULTICORE configuration consists of one or two numbers (default 1):
   THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4.
 """,
         "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),
         "P:" -> (arg => afp_partition = Value.Int.parse(arg)),
         "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
         "e:" -> (arg => more_settings = more_settings ::: List(arg)),
         "f" -> (_ => fresh = true),
         "h:" -> (arg => hostname = arg),
         "i:" -> (arg => init_settings = init_settings ::: List(arg)),
         "m:" ->
           {
             case "32" | "x86" => arch_64 = false
             case "64" | "x86_64" => arch_64 = true
             case bad => error("Bad processor architecture: " + quote(bad))
           },
         "o:" -> (arg => output_file = arg),
         "r:" -> (arg => rev = arg),
         "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
         "t:" -> (arg => build_tags = build_tags ::: List(arg)),
         "u:" -> (arg => user_home = Path.explode(arg)),
         "v" -> (_ => verbose = true),
         "x" -> (_ => exit_code = true))
 
       val more_args = getopts(args)
       val (root, build_args) =
         more_args match {
           case root :: build_args => (Path.explode(root), build_args)
           case _ => getopts.usage()
         }
 
       val progress = new Console_Progress(stderr = true)
 
       val results =
         build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
           afp_rev = afp_rev, afp_partition = afp_partition,
           isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
           components_base = components_base, fresh = fresh, hostname = hostname,
           multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
           heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
           max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
           verbose = verbose, build_tags = build_tags, build_args = build_args)
 
       if (output_file == "") {
         for ((_, log_path) <- results)
           Output.writeln(log_path.implode, stdout = true)
       }
       else {
         File.write(Path.explode(output_file),
           cat_lines(for ((_, log_path) <- results) yield log_path.implode))
       }
 
       val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
       if (rc != 0 && exit_code) sys.exit(rc)
     }
   }
 
 
 
   /** remote build_history -- via command-line **/
 
   def remote_build_history(
     ssh: SSH.Session,
     isabelle_repos_self: Path,
     isabelle_repos_other: Path,
     isabelle_repos_source: String = Isabelle_Cronjob.isabelle_repos_source,
     afp_repos_source: String = AFP.repos_source,
     isabelle_identifier: String = "remote_build_history",
     self_update: Boolean = false,
     progress: Progress = No_Progress,
     rev: String = "",
     afp_rev: Option[String] = None,
     options: String = "",
     args: String = ""): List[(String, Bytes)] =
   {
     /* Isabelle self repository */
 
     val self_hg =
       Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = ssh)
 
     def execute(cmd: String, args: String, echo: Boolean = false, strict: Boolean = true): Unit =
       ssh.execute(
         Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
           ssh.bash_path(isabelle_repos_self + Path.explode(cmd)) + " " + args,
         progress_stdout = progress.echo_if(echo, _),
         progress_stderr = progress.echo_if(echo, _),
         strict = strict).check
 
     if (self_update) {
       val hg = Mercurial.repository(Path.explode("~~"))
       hg.push(self_hg.root_url, force = true)
       self_hg.update(rev = hg.parent(), clean = true)
 
       execute("bin/isabelle", "components -I")
       execute("bin/isabelle", "components -a", echo = true)
       execute("Admin/build", "jars_fresh")
     }
 
     val rev_id = self_hg.id(rev)
 
 
     /* Isabelle other + AFP repository */
 
     if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) {
       ssh.rm_tree(isabelle_repos_other)
     }
     val other_hg =
       Mercurial.clone_repository(
         ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev_id, ssh = ssh)
 
     val afp_options =
       if (afp_rev.isEmpty) ""
       else {
         val afp_repos = isabelle_repos_other + Path.explode("AFP")
         val afp_hg = Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh)
         " -A " + Bash.string(afp_rev.get)
       }
 
 
     /* Admin/build_history */
 
     ssh.with_tmp_dir(tmp_dir =>
     {
       val output_file = tmp_dir + Path.explode("output")
 
       execute("Admin/build_history",
         "-o " + ssh.bash_path(output_file) +
           (if (rev == "") "" else " -r " + Bash.string(rev_id)) + " " +
           options + afp_options + " " + ssh.bash_path(isabelle_repos_other) + " " + args,
         echo = true, strict = false)
 
       for (line <- split_lines(ssh.read(output_file)))
       yield {
         val log = Path.explode(line)
         val bytes = ssh.read_bytes(log)
         ssh.rm(log)
         (log.file_name, bytes)
       }
     })
   }
 }
diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala
+++ b/src/Pure/Admin/build_release.scala
@@ -1,776 +1,777 @@
 /*  Title:      Pure/Admin/build_release.scala
     Author:     Makarius
 
 Build full Isabelle distribution from repository.
 */
 
 package isabelle
 
 
 object Build_Release
 {
   /** release info **/
 
   sealed case class Bundle_Info(
     platform: Platform.Family.Value,
     platform_description: String,
     name: String)
   {
     def path: Path = Path.explode(name)
   }
 
   class Release private[Build_Release](
     progress: Progress,
     val date: Date,
     val dist_name: String,
     val dist_dir: Path,
     val dist_version: String,
     val ident: String)
   {
     val isabelle_dir: Path = dist_dir + Path.explode(dist_name)
     val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
     val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
 
     def other_isabelle(dir: Path): Other_Isabelle =
       Other_Isabelle(dir + Path.explode(dist_name),
         isabelle_identifier = dist_name + "-build",
         progress = progress)
 
     def bundle_info(platform: Platform.Family.Value): Bundle_Info =
       platform match {
         case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
         case Platform.Family.macos => Bundle_Info(platform, "Mac OS X", dist_name + "_macos.tar.gz")
         case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
       }
   }
 
 
 
   /** generated content **/
 
   /* patch release */
 
   private def change_file(dir: Path, name: String, f: String => String)
   {
     val file = dir + Path.explode(name)
     File.write(file, f(File.read(file)))
   }
 
   private val getsettings_file: String = "lib/scripts/getsettings"
 
   private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r
 
   def patch_release(release: Release, is_official: Boolean)
   {
     val dir = release.isabelle_dir
 
     for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala"))
     {
       change_file(dir, name,
         s =>
           s.replaceAllLiterally("val is_identified = false", "val is_identified = true")
            .replaceAllLiterally("val is_official = false", "val is_official = " + is_official))
     }
 
     change_file(dir, getsettings_file,
       s =>
         s.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
          .replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"",
             "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
 
     change_file(dir, "lib/html/library_index_header.template",
       s => s.replaceAllLiterally("{ISABELLE}", release.dist_name))
 
     for {
       name <-
         List(
           "src/Pure/System/distribution.ML",
           "src/Pure/System/distribution.scala",
           "lib/Tools/version") }
     {
       change_file(dir, name,
         s => s.replaceAllLiterally("repository version", release.dist_version))
     }
 
     change_file(dir, "README",
       s => s.replaceAllLiterally("some repository version of Isabelle", release.dist_version))
   }
 
 
   /* ANNOUNCE */
 
   def make_announce(release: Release)
   {
     File.write(release.isabelle_dir + Path.explode("ANNOUNCE"),
 """
 IMPORTANT NOTE
 ==============
 
 This is a snapshot of Isabelle/""" + release.ident + """ from the repository.
 
 """)
   }
 
 
   /* NEWS */
 
   def make_news(other_isabelle: Other_Isabelle, dist_version: String)
   {
     val target = other_isabelle.isabelle_home + Path.explode("doc")
     val target_fonts = target + Path.explode("fonts")
     Isabelle_System.mkdirs(target_fonts)
     other_isabelle.copy_fonts(target_fonts)
 
     HTML.write_document(target, "NEWS.html",
       List(HTML.title("NEWS (" + dist_version + ")")),
       List(
         HTML.chapter("NEWS"),
         HTML.source(
           Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS"))))))
   }
 
 
   /* bundled components */
 
   class Bundled(platform: Option[Platform.Family.Value] = None)
   {
     def detect(s: String): Boolean =
       s.startsWith("#bundled") && !s.startsWith("#bundled ")
 
     def apply(name: String): String =
       "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name
 
     private val Pattern1 = ("""^#bundled:(.*)$""").r
     private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
 
     def unapply(s: String): Option[String] =
       s match {
         case Pattern1(name) => Some(name)
         case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name)
         case _ => None
       }
   }
 
   def record_bundled_components(dir: Path)
   {
     val catalogs =
       List("main", "bundled").map((_, new Bundled())) :::
       default_platform_families.flatMap(platform =>
         List(platform.toString, "bundled-" + platform.toString).
           map((_, new Bundled(platform = Some(platform)))))
 
     File.append(Components.components(dir),
       terminate_lines("#bundled components" ::
         (for {
           (catalog, bundled) <- catalogs.iterator
           val path = Components.admin(dir) + Path.basic(catalog)
           if path.is_file
           line <- split_lines(File.read(path))
           if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
         } yield bundled(line)).toList))
   }
 
   def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) =
   {
     val Bundled = new Bundled(platform = Some(platform))
     val components =
       for {
         Bundled(name) <- Components.read_components(dir)
         if !name.startsWith("jedit_build")
       } yield name
     val jdk_component =
       components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
     (components, jdk_component)
   }
 
   def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String])
   {
     def contrib_name(name: String): String =
       Components.contrib(name = name).implode
 
     val Bundled = new Bundled(platform = Some(platform))
     Components.write_components(dir,
       Components.read_components(dir).flatMap(line =>
         line match {
           case Bundled(name) =>
             if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
             else None
           case _ => if (Bundled.detect(line)) None else Some(line)
         }) ::: more_names.map(contrib_name(_)))
   }
 
   def make_contrib(dir: Path)
   {
     Isabelle_System.mkdirs(Components.contrib(dir))
     File.write(Components.contrib(dir, "README"),
 """This directory contains add-on components that contribute to the main
 Isabelle distribution.  Separate licensing conditions apply, see each
 directory individually.
 """)
   }
 
 
 
   /** build_release **/
 
   private def execute(dir: Path, script: String): Unit =
     Isabelle_System.bash(script, cwd = dir.file).check
 
   private def execute_tar(dir: Path, args: String): Unit =
     Isabelle_System.gnutar(args, dir = dir).check
 
   private val default_platform_families: List[Platform.Family.Value] =
     List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
 
   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 = "",
     official_release: Boolean = false,
     proper_release_name: Option[String] = None,
     platform_families: List[Platform.Family.Value] = default_platform_families,
     more_components: List[Path] = Nil,
     website: Option[Path] = None,
     build_library: Boolean = false,
     parallel_jobs: Int = 1): Release =
   {
     val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME"))
 
     val release =
     {
       val date = Date.now()
       val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date))
       val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute
 
       val version = proper_string(rev) orElse proper_release_name getOrElse "tip"
       val ident =
         try { hg.id(version) }
         catch { case ERROR(_) => error("Bad repository version: " + version) }
 
       val dist_version =
         proper_release_name match {
           case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date)
           case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
         }
 
       new Release(progress, date, dist_name, dist_dir, dist_version, ident)
     }
 
 
     /* make distribution */
 
     if (release.isabelle_archive.is_file) {
       progress.echo_warning("Release archive already exists: " + release.isabelle_archive)
 
       val archive_ident =
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
           {
             val getsettings = Path.explode(release.dist_name + "/" + getsettings_file)
             execute_tar(tmp_dir, "-xzf " +
               File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
             split_lines(File.read(tmp_dir + getsettings))
               .collectFirst({ case ISABELLE_ID(ident) => ident })
               .getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive))
           })
 
       if (release.ident != archive_ident) {
         error("Mismatch of release identification " + release.ident +
           " vs. archive " + archive_ident)
       }
     }
     else {
       progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...")
 
       Isabelle_System.mkdirs(release.dist_dir)
 
       if (release.isabelle_dir.is_dir)
         error("Directory " + release.isabelle_dir + " already exists")
 
 
       progress.echo_warning("Retrieving Mercurial repository version " + release.ident)
 
       hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files")
 
       for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
         (release.isabelle_dir + Path.explode(name)).file.delete
       }
 
 
       progress.echo_warning("Preparing distribution " + quote(release.dist_name))
 
       patch_release(release, proper_release_name.isDefined && official_release)
 
       if (proper_release_name.isEmpty) make_announce(release)
 
       make_contrib(release.isabelle_dir)
 
       execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
 
       record_bundled_components(release.isabelle_dir)
 
 
       /* build tools and documentation */
 
       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 {
         val export_classpath =
           "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
         other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
         other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
       }
       catch { case ERROR(_) => error("Failed to build tools") }
 
       try {
         other_isabelle.bash(
           "./bin/isabelle build_doc -a -s -j " + parallel_jobs, echo = true).check
       }
       catch { case ERROR(_) => error("Failed to build documentation") }
 
       make_news(other_isabelle, release.dist_version)
 
       for (name <- List("Admin", "browser_info", "heaps")) {
         Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
       }
 
       other_isabelle.cleanup()
 
 
       progress.echo_warning("Creating distribution archive " + release.isabelle_archive)
 
       def execute_dist_name(script: String): Unit =
         Isabelle_System.bash(script, cwd = release.dist_dir.file,
           env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check
 
       execute_dist_name("""
 set -e
 
 chmod -R a+r "$DIST_NAME"
 chmod -R u+w "$DIST_NAME"
 chmod -R g=o "$DIST_NAME"
 find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
 """)
 
       execute_tar(release.dist_dir, "-czf " +
         File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
 
       execute_dist_name("""
 set -e
 
 mv "$DIST_NAME" "${DIST_NAME}-old"
 mkdir "$DIST_NAME"
 
 mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \
   "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME"
 mkdir "$DIST_NAME/doc"
 mv "${DIST_NAME}-old/doc/"*.pdf \
   "${DIST_NAME}-old/doc/"*.html \
   "${DIST_NAME}-old/doc/"*.css \
   "${DIST_NAME}-old/doc/fonts" \
   "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
 
 rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
 
 rm -rf "${DIST_NAME}-old"
 """)
     }
 
 
     /* make application bundles */
 
     val bundle_infos = platform_families.map(release.bundle_info)
 
     for (bundle_info <- bundle_infos) {
       val bundle_archive = release.dist_dir + bundle_info.path
       if (bundle_archive.is_file && more_components.isEmpty)
         progress.echo_warning("Application bundle already exists: " + bundle_archive)
       else {
         val isabelle_name = release.dist_name
         val platform = bundle_info.platform
 
         progress.echo("\nApplication bundle for " + platform)
 
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
         {
           // release archive
 
           execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
           val other_isabelle = release.other_isabelle(tmp_dir)
           val isabelle_target = other_isabelle.isabelle_home
 
 
           // bundled components
 
           progress.echo("Bundled components:")
 
           val contrib_dir = Components.contrib(isabelle_target)
 
           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))
 
           Components.purge(contrib_dir, platform)
 
           activate_components(isabelle_target, platform, more_components_names)
 
 
           // Java parameters
 
           val java_options_title = "# Java runtime options"
           val java_options: List[String] =
             (for {
               variable <-
                 List(
                   "ISABELLE_JAVA_SYSTEM_OPTIONS",
                   "JEDIT_JAVA_SYSTEM_OPTIONS",
                   "JEDIT_JAVA_OPTIONS")
               opt <- Word.explode(other_isabelle.getenv(variable))
             } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name)
 
           val classpath: List[Path] =
           {
             val base = isabelle_target.absolute
             Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
             {
               val abs_path = path.absolute
               File.relative_path(base, abs_path) match {
                 case Some(rel_path) => rel_path
                 case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
               }
             }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
           }
 
           val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
 
 
           // application bundling
 
           platform match {
             case Platform.Family.linux =>
               File.write(isabelle_target + Path.explode(isabelle_name + ".options"),
                 terminate_lines(java_options_title :: java_options))
 
               val isabelle_run = isabelle_target + Path.explode(isabelle_name + ".run")
               File.write(isabelle_run,
                 File.read(Path.explode("~~/Admin/Linux/Isabelle.run"))
                   .replaceAllLiterally("{CLASSPATH}",
                     classpath.map("$ISABELLE_HOME/" + _).mkString(":"))
                   .replaceAllLiterally("/jdk/", "/" + jdk_component + "/"))
               File.executable(isabelle_run)
 
               val linux_app = isabelle_target + Path.explode("contrib/linux_app")
               File.move(linux_app + Path.explode("Isabelle"),
                 isabelle_target + Path.explode(isabelle_name))
               Isabelle_System.rm_tree(linux_app)
 
               val archive_name = isabelle_name + "_linux.tar.gz"
               progress.echo("Packaging " + archive_name + " ...")
               execute_tar(tmp_dir,
                 "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
                 Bash.string(isabelle_name))
 
 
             case Platform.Family.macos =>
               File.write(isabelle_target + jedit_props,
                 File.read(isabelle_target + jedit_props)
                   .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
                   .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
                   .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
                   .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
 
 
               // MacOS application bundle
 
               File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
 
               val isabelle_app = Path.explode(isabelle_name + ".app")
               val app_dir = tmp_dir + isabelle_app
               File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir)
 
               val app_contents = app_dir + Path.explode("Contents")
               val app_resources = app_contents + Path.explode("Resources")
               File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
 
               File.write(app_contents + Path.explode("Info.plist"),
                 File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
                   .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
                   .replaceAllLiterally("{JAVA_OPTIONS}",
                     terminate_lines(java_options.map(opt => "<string>" + opt + "</string>"))))
 
               for (cp <- classpath) {
                 File.link(
                   Path.explode("../Resources/" + isabelle_name + "/") + cp,
                   app_contents + Path.explode("Java"),
                   force = true)
               }
 
               File.link(
                 Path.explode("../Resources/" + isabelle_name + "/contrib/" +
                   jdk_component + "/x86_64-darwin"),
                 app_contents + Path.explode("PlugIns/bundled.jdk"),
                 force = true)
 
               File.link(
                 Path.explode("../../Info.plist"),
                 app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"),
                 force = true)
 
               File.link(
                 Path.explode("Contents/Resources/" + isabelle_name),
                 app_dir + Path.explode("Isabelle"),
                 force = true)
 
 
               // application archive
 
               val archive_name = isabelle_name + "_macos.tar.gz"
               progress.echo("Packaging " + archive_name + " ...")
               execute_tar(tmp_dir,
                 "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
                 File.bash_path(isabelle_app))
 
 
             case Platform.Family.windows =>
               File.write(isabelle_target + jedit_props,
                 File.read(isabelle_target + jedit_props)
                   .replaceAll("lookAndFeel=.*",
                     "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
                   .replaceAll("foldPainter=.*", "foldPainter=Square"))
 
 
               // application launcher
 
               File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
 
               val app_template = Path.explode("~~/Admin/Windows/launch4j")
 
               File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
                 (java_options_title :: java_options).map(_ + "\r\n").mkString)
 
               val isabelle_xml = Path.explode("isabelle.xml")
               val isabelle_exe = Path.explode(isabelle_name + ".exe")
 
               File.write(tmp_dir + isabelle_xml,
                 File.read(app_template + isabelle_xml)
                   .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
                   .replaceAllLiterally("{OUTFILE}",
                     File.platform_path(isabelle_target + isabelle_exe))
                   .replaceAllLiterally("{ICON}",
                     File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
                   .replaceAllLiterally("{SPLASH}",
                     File.platform_path(app_template + Path.explode("isabelle.bmp")))
                   .replaceAllLiterally("{CLASSPATH}",
                     cat_lines(classpath.map(cp =>
                       "    <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>")))
                   .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
 
               execute(tmp_dir,
                 "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
 
               File.copy(app_template + Path.explode("manifest.xml"),
                 isabelle_target + isabelle_exe.ext("manifest"))
 
 
               // Cygwin setup
 
               val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
 
               File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
 
               val cygwin_mirror =
                 File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
 
               val cygwin_bat = Path.explode("Cygwin-Setup.bat")
               File.write(isabelle_target + cygwin_bat,
                 File.read(cygwin_template + cygwin_bat)
                   .replaceAllLiterally("{MIRROR}", cygwin_mirror))
               File.executable(isabelle_target + cygwin_bat)
 
               for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
                 val path = Path.explode(name)
                 File.copy(cygwin_template + path,
                   isabelle_target + Path.explode("contrib/cygwin") + path)
               }
 
               execute(isabelle_target,
                 """find . -type f -not -name "*.exe" -not -name "*.dll" """ +
                 (if (Platform.is_macos) "-perm +100" else "-executable") +
                 " -print0 > contrib/cygwin/isabelle/executables")
 
               execute(isabelle_target,
                 """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
                 """> contrib/cygwin/isabelle/symlinks""")
 
               execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
 
               File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
 
 
               // executable archive (self-extracting 7z)
 
               val exe_archive = tmp_dir + Path.explode(isabelle_name + ".7z")
               exe_archive.file.delete
 
               execute(tmp_dir,
                 "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
               if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
 
               val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
               val sfx_txt =
                 File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")).
                   replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
 
               Bytes.write(release.dist_dir + isabelle_exe,
                 Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
               File.executable(release.dist_dir + isabelle_exe)
           }
         })
         progress.echo("DONE")
       }
     }
 
 
     /* minimal website */
 
     for (dir <- website) {
       val website_platform_bundles =
         for {
           bundle_info <- bundle_infos
           if (release.dist_dir + bundle_info.path).is_file
         } yield (bundle_info.name, bundle_info)
 
       val afp_link =
         HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev))
 
       HTML.write_document(dir, "index.html",
         List(HTML.title(release.dist_name)),
         List(
           HTML.chapter(release.dist_name + " (" + release.ident + ")"),
           HTML.itemize(
             website_platform_bundles.map({ case (bundle, bundle_info) =>
               List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) :::
         (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link)))))
 
       for ((bundle, _) <- website_platform_bundles)
         File.copy(release.dist_dir + Path.explode(bundle), dir)
     }
 
 
     /* HTML library */
 
     if (build_library) {
       if (release.isabelle_library_archive.is_file) {
         progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive)
       }
       else {
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
           {
             val bundle =
               release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz")
             execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
 
             val other_isabelle = release.other_isabelle(tmp_dir)
 
             Isabelle_System.mkdirs(other_isabelle.etc)
             File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
 
             other_isabelle.bash("bin/isabelle build -j " + parallel_jobs +
               " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
               " -s -c -a -d '~~/src/Benchmarks'", echo = true).check
             other_isabelle.isabelle_home_user.file.delete
 
             execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
             execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
             execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) +
               " " + Bash.string(release.dist_name + "/browser_info"))
           })
       }
     }
 
     release
   }
 
 
 
   /** command line entry point **/
 
   def main(args: Array[String])
   {
     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
       var more_components: List[Path] = Nil
       var parallel_jobs = 1
       var build_library = false
       var options = Options.init()
       var platform_families = default_platform_families
       var rev = ""
 
       val getopts = Getopts("""
 Usage: Admin/build_release [OPTIONS] BASE_DIR
 
   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
     -c ARCHIVE   clean bundling with additional component .tar.gz archive
     -j INT       maximum number of parallel jobs (default 1)
     -l           build library
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p NAMES     platform families (default: """ + default_platform_families.mkString(",") + """)
     -r REV       Mercurial changeset id (default: RELEASE or tip)
 
   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))),
         "c:" -> (arg =>
           {
             val path = Path.explode(arg)
             Components.Archive.get_name(path.file_name)
             more_components = more_components ::: List(path)
           }),
         "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
         "l" -> (_ => build_library = true),
         "o:" -> (arg => options = options + arg),
         "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)),
         "r:" -> (arg => rev = arg))
 
       val more_args = getopts(args)
       val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() }
 
       val progress = new Console_Progress()
 
       if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
         error("Building for windows requires 7z")
 
       build_release(Path.explode(base_dir), options, components_base = components_base,
         progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release,
         proper_release_name = proper_release_name, website = website,
         platform_families =
           if (platform_families.isEmpty) default_platform_families
           else platform_families,
         more_components = more_components, build_library = build_library,
         parallel_jobs = parallel_jobs)
     }
   }
 }
diff --git a/src/Pure/Admin/components.scala b/src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala
+++ b/src/Pure/Admin/components.scala
@@ -1,293 +1,295 @@
 /*  Title:      Pure/Admin/components.scala
     Author:     Makarius
 
 Isabelle system components.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 
 
 object Components
 {
   /* archive name */
 
   object Archive
   {
     val suffix: String = ".tar.gz"
 
     def apply(name: String): String =
       if (name == "") error("Bad component name: " + quote(name))
       else name + suffix
 
     def unapply(archive: String): Option[String] =
     {
       for {
         name0 <- Library.try_unsuffix(suffix, archive)
         name <- proper_string(name0)
       } yield name
     }
 
     def get_name(archive: String): String =
       unapply(archive) getOrElse
         error("Bad component archive name (expecting .tar.gz): " + quote(archive))
   }
 
 
   /* 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 =
     dir + Path.explode("contrib") + Path.explode(name)
 
   def unpack(dir: Path, archive: Path, progress: Progress = No_Progress): String =
   {
     val name = Archive.get_name(archive.file_name)
     progress.echo("Unpacking " + name)
     Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
     name
   }
 
   def resolve(base_dir: Path, names: List[String],
     target_dir: Option[Path] = None,
     progress: Progress = No_Progress)
   {
     Isabelle_System.mkdirs(base_dir)
     for (name <- names) {
       val archive_name = Archive(name)
       val archive = base_dir + Path.explode(archive_name)
       if (!archive.is_file) {
         val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive_name
         progress.echo("Getting " + remote)
         Bytes.write(archive, Url.read_bytes(Url(remote)))
       }
       unpack(target_dir getOrElse base_dir, archive, progress = progress)
     }
   }
 
   def purge(dir: Path, platform: Platform.Family.Value)
   {
     def purge_platforms(platforms: String*): Set[String] =
       platforms.flatMap(name => List("x86-" + name, "x86_64-" + name)).toSet + "ppc-darwin"
     val purge_set =
       platform match {
         case Platform.Family.linux => purge_platforms("darwin", "cygwin", "windows")
         case Platform.Family.macos => purge_platforms("linux", "cygwin", "windows")
         case Platform.Family.windows => purge_platforms("linux", "darwin")
       }
 
     File.find_files(dir.file,
       (file: JFile) => file.isDirectory && purge_set(file.getName),
       include_dirs = true).foreach(Isabelle_System.rm_tree)
   }
 
 
   /* component directory content */
 
   def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings")
   def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components")
 
   def check_dir(dir: Path): Boolean =
     settings(dir).is_file || components(dir).is_file
 
   def read_components(dir: Path): List[String] =
     split_lines(File.read(components(dir))).filter(_.nonEmpty)
 
   def write_components(dir: Path, lines: List[String]): Unit =
     File.write(components(dir), terminate_lines(lines))
 
 
   /* component repository content */
 
   val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1")
 
   sealed case class SHA1_Digest(sha1: String, file_name: String)
   {
     override def toString: String = sha1 + "  " + file_name
   }
 
   def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] =
     (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line =>
       Word.explode(line) match {
         case Nil => None
         case List(sha1, name) => Some(SHA1_Digest(sha1, name))
         case _ => error("Bad components.sha1 entry: " + quote(line))
       })
 
   def write_components_sha1(entries: List[SHA1_Digest]) =
     File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n"))
 
 
 
   /** build and publish components **/
 
   def build_components(
     options: Options,
     components: List[Path],
     progress: Progress = No_Progress,
     publish: Boolean = false,
     force: Boolean = false,
     update_components_sha1: Boolean = false)
   {
     val archives: List[Path] =
       for (path <- components) yield {
         path.file_name match {
           case Archive(_) => path
           case name =>
             if (!path.is_dir) error("Bad component directory: " + path)
             else if (!check_dir(path)) {
               error("Malformed component directory: " + path +
                 "\n  (requires " + settings() + " or " + Components.components() + ")")
             }
             else {
               val component_path = path.expand
               val archive_dir = component_path.dir
               val archive_name = Archive(name)
 
               val archive = archive_dir + Path.explode(archive_name)
               if (archive.is_file && !force) {
                 error("Component archive already exists: " + archive)
               }
 
               progress.echo("Packaging " + archive_name + " ...")
               Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name),
                 dir = archive_dir).check
 
               archive
             }
         }
       }
 
     if ((publish && archives.nonEmpty) || update_components_sha1) {
       options.string("isabelle_components_server") match {
         case SSH.Target(user, host) =>
           using(SSH.open_session(options, host = host, user = user))(ssh =>
           {
             val components_dir = Path.explode(options.string("isabelle_components_dir"))
             val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir"))
 
             for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) {
               error("Bad remote directory: " + dir)
             }
 
             if (publish) {
               for (archive <- archives) {
                 val archive_name = archive.file_name
                 val name = Archive.get_name(archive_name)
                 val remote_component = components_dir + archive.base
                 val remote_contrib = contrib_dir + Path.explode(name)
 
                 // component archive
                 if (ssh.is_file(remote_component) && !force) {
                   error("Remote component archive already exists: " + remote_component)
                 }
                 progress.echo("Uploading " + archive_name)
                 ssh.write_file(remote_component, archive)
 
                 // contrib directory
                 val is_standard_component =
                   Isabelle_System.with_tmp_dir("component")(tmp_dir =>
                   {
                     Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
                     check_dir(tmp_dir + Path.explode(name))
                   })
                 if (is_standard_component) {
                   if (ssh.is_dir(remote_contrib)) {
                     if (force) ssh.rm_tree(remote_contrib)
                     else error("Remote component directory already exists: " + remote_contrib)
                   }
                   progress.echo("Unpacking remote " + archive_name)
                   ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " +
                     ssh.bash_path(remote_component)).check
                 }
                 else {
                   progress.echo_warning("No unpacking of non-standard component: " + archive_name)
                 }
               }
             }
 
             // remote SHA1 digests
             if (update_components_sha1) {
               val lines =
                 for {
                   entry <- ssh.read_dir(components_dir)
                   if entry.is_file && entry.name.endsWith(Archive.suffix)
                 }
                 yield {
                   progress.echo("Digesting remote " + entry.name)
                   Library.trim_line(
                     ssh.execute("cd " + ssh.bash_path(components_dir) +
                       "; sha1sum " + Bash.string(entry.name)).check.out)
                 }
               write_components_sha1(read_components_sha1(lines))
             }
           })
         case s => error("Bad isabelle_components_server: " + quote(s))
       }
     }
 
     // local SHA1 digests
     {
       val new_entries =
         for (archive <- archives)
         yield {
           val file_name = archive.file_name
           progress.echo("Digesting local " + file_name)
           val sha1 = SHA1.digest(archive).rep
           SHA1_Digest(sha1, file_name)
         }
       val new_names = new_entries.map(_.file_name).toSet
 
       write_components_sha1(
         new_entries :::
         read_components_sha1().filterNot(entry => new_names.contains(entry.file_name)))
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   private val relevant_options =
     List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir")
 
   val isabelle_tool =
     Isabelle_Tool("build_components", "build and publish Isabelle components", args =>
     {
       var publish = false
       var update_components_sha1 = false
       var force = false
       var options = Options.init()
 
       def show_options: String =
         cat_lines(relevant_options.map(name => options.options(name).print))
 
       val getopts = Getopts("""
 Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS...
 
   Options are:
     -P           publish on SSH server (see options below)
     -f           force: overwrite existing component archives and directories
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -u           update all SHA1 keys in Isabelle repository Admin/components
 
   Build and publish Isabelle components as .tar.gz archives on SSH server,
   depending on system options:
 
 """ + Library.prefix_lines("  ", show_options) + "\n",
         "P" -> (_ => publish = true),
         "f" -> (_ => force = true),
         "o:" -> (arg => options = options + arg),
         "u" -> (_ => update_components_sha1 = true))
 
       val more_args = getopts(args)
       if (more_args.isEmpty && !update_components_sha1) getopts.usage()
 
       val progress = new Console_Progress
 
       build_components(options, more_args.map(Path.explode), progress = progress,
         publish = publish, force = force, update_components_sha1 = update_components_sha1)
     })
 }
diff --git a/src/Pure/Admin/other_isabelle.scala b/src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala
+++ b/src/Pure/Admin/other_isabelle.scala
@@ -1,118 +1,115 @@
 /*  Title:      Pure/Admin/other_isabelle.scala
     Author:     Makarius
 
 Manage other Isabelle distributions.
 */
 
 package isabelle
 
 
 object Other_Isabelle
 {
   def apply(isabelle_home: Path,
       isabelle_identifier: String = "",
       user_home: Path = Path.explode("$USER_HOME"),
       progress: Progress = No_Progress): Other_Isabelle =
     new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress)
 }
 
 class Other_Isabelle(
   val isabelle_home: Path,
   val isabelle_identifier: String,
   user_home: Path,
   progress: Progress)
 {
   other_isabelle =>
 
   override def toString: String = isabelle_home.toString
 
   if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined)
     error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
 
 
   /* static system */
 
   def bash(
       script: String,
       redirect: Boolean = false,
       echo: Boolean = false,
       strict: Boolean = true): Process_Result =
     progress.bash(
       "export USER_HOME=" + File.bash_path(user_home) + "\n" +
       Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
       env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
 
   def apply(
       cmdline: String,
       redirect: Boolean = false,
       echo: Boolean = false,
       strict: Boolean = true): Process_Result =
     bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict)
 
   def resolve_components(echo: Boolean): Unit =
     other_isabelle("components -a", redirect = true, echo = echo).check
 
   def getenv(name: String): String =
     other_isabelle("getenv -b " + Bash.string(name)).check.out
 
   val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER"))
 
   val etc: Path = isabelle_home_user + Path.explode("etc")
   val etc_settings: Path = etc + Path.explode("settings")
   val etc_preferences: Path = etc + Path.explode("preferences")
 
   def copy_fonts(target_dir: Path): Unit =
     Isabelle_Fonts.make_entries(getenv = getenv(_), hidden = true).
       foreach(entry => File.copy(entry.path, target_dir))
 
 
   /* 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)))
   }
 
 
   /* settings */
 
   def clean_settings(): Boolean =
     if (!etc_settings.is_file) true
     else if (File.read(etc_settings).startsWith("# generated by Isabelle")) {
       etc_settings.file.delete; true
     }
     else false
 
   def init_settings(settings: List[String])
   {
     if (!clean_settings())
       error("Cannot proceed with existing user settings file: " + etc_settings)
 
     Isabelle_System.mkdirs(etc_settings.dir)
     File.write(etc_settings,
       "# generated by Isabelle " + Date.now() + "\n" +
       "#-*- shell-script -*- :mode=shellscript:\n" +
       settings.mkString("\n", "\n", "\n"))
   }
 
 
   /* cleanup */
 
   def cleanup()
   {
     clean_settings()
     etc.file.delete
     isabelle_home_user.file.delete
   }
 }