# 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>\<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