# HG changeset patch # User wenzelm # Date 1616869594 -3600 # Node ID 4f8849357ba73ea541c49be8a51edf906d51e69f # Parent 804e75127f29580af6377ef4d207be43b456ff2d more robust: idempotent; diff -r 804e75127f29 -r 4f8849357ba7 lib/Tools/components --- 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 diff -r 804e75127f29 -r 4f8849357ba7 src/Doc/System/Misc.thy --- 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>\-I\ 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>\init_components\\\\\<^verbatim>\components/main\'' needs + to be edited according to the printed explanation. \<^medskip> Options \<^verbatim>\-u\ and \<^verbatim>\-x\ operate on user components listed in