more robust: idempotent;
authorwenzelm
Sat, 27 Mar 2021 19:26:34 +0100
changeset 73739 4f8849357ba7
parent 73738 804e75127f29
child 73740 3cbf041f544a
more robust: idempotent;
lib/Tools/components
src/Doc/System/Misc.thy
--- 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