--- a/lib/Tools/components Sat Mar 27 18:15:19 2021 +0100
+++ b/lib/Tools/components Sat Mar 27 19:26:34 2021 +0100
@@ -98,8 +98,19 @@
if [ -n "$INIT_SETTINGS" ]; then
SETTINGS="$ISABELLE_HOME_USER/etc/settings"
- SETTINGS_CONTENT='init_components "$ISABELLE_COMPONENTS_BASE" "$ISABELLE_HOME/Admin/components/main"'
- if [ -e "$SETTINGS" ]; then
+ SETTINGS_CONTENT='init_components "${ISABELLE_COMPONENTS_BASE:-$USER_HOME/.isabelle/contrib}" "$ISABELLE_HOME/Admin/components/main"'
+ if [ ! -e "$SETTINGS" ]; then
+ echo "Initializing \"$SETTINGS\""
+ mkdir -p "$(dirname "$SETTINGS")"
+ {
+ echo "#-*- shell-script -*- :mode=shellscript:"
+ echo
+ echo "$SETTINGS_CONTENT"
+ } > "$SETTINGS"
+ elif grep "init_components.*components/main" "$SETTINGS" >/dev/null 2>/dev/null
+ then
+ :
+ else
echo "User settings file already exists!"
echo
echo "Edit \"$SETTINGS\" manually"
@@ -107,14 +118,6 @@
echo
echo " $SETTINGS_CONTENT"
echo
- else
- echo "Initializing \"$SETTINGS\""
- mkdir -p "$(dirname "$SETTINGS")"
- {
- echo "#-*- shell-script -*- :mode=shellscript:"
- echo
- echo "$SETTINGS_CONTENT"
- } > "$SETTINGS"
fi
elif [ -n "$LIST_ONLY" ]; then
echo
--- a/src/Doc/System/Misc.thy Sat Mar 27 18:15:19 2021 +0100
+++ b/src/Doc/System/Misc.thy Sat Mar 27 19:26:34 2021 +0100
@@ -164,8 +164,9 @@
\<^medskip>
Option \<^verbatim>\<open>-I\<close> initializes the user settings file to subscribe to the standard
components specified in the Isabelle repository clone --- this does not make
- any sense for regular Isabelle releases. If the file already exists, it
- needs to be edited manually according to the printed explanation.
+ any sense for regular Isabelle releases. An existing file that does not
+ contain a suitable line ``\<^verbatim>\<open>init_components\<close>\<open>\<dots>\<close>\<^verbatim>\<open>components/main\<close>'' needs
+ to be edited according to the printed explanation.
\<^medskip>
Options \<^verbatim>\<open>-u\<close> and \<^verbatim>\<open>-x\<close> operate on user components listed in