more modular shell script;

--- a/lib/Tools/components	Mon Jan 23 14:26:42 2023 +0100
+++ b/lib/Tools/components	Mon Jan 23 15:15:19 2023 +0100
@@ -130,6 +130,7 @@
   isabelle scala_build || exit $?
   exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}"
 else
+  source "$ISABELLE_HOME/lib/scripts/download_file"
   for NAME in "${SELECTED_COMPONENTS[@]}"
   do
     BASE_NAME="$(basename "$NAME")"
@@ -144,26 +145,7 @@
       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_OPTIONS="--fail --silent --location"
-        if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then
-          case $(sw_vers -productVersion) in
-            10.*)
-              CURL_OPTIONS="$CURL_OPTIONS --insecure"
-              ;;
-          esac
-        fi
-        if curl $CURL_OPTIONS "$REMOTE" > "${FULL_NAME}.tar.gz.part"
-        then
-          mv -f "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
-        else
-          rm -f "${FULL_NAME}.tar.gz.part"
-          fail "Failed to download \"$REMOTE\""
-        fi
+        download_file "$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz" "${FULL_NAME}.tar.gz" || exit $?
       fi
       if [ -e "${FULL_NAME}.tar.gz" ]; then
         echo "Unpacking \"${FULL_NAME}.tar.gz\""

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/download_file	Mon Jan 23 15:15:19 2023 +0100
@@ -0,0 +1,40 @@
+# -*- shell-script -*- :mode=shellscript:
+#
+# Bash function to download file via "curl".
+
+function download_file ()
+{
+  [ "$#" -ne 2 ] && {
+    echo "Bad arguments for download_file" >&2
+    return 2
+  }
+  local REMOTE="$1"
+  local LOCAL="$2"
+
+  type -p curl > /dev/null || {
+    echo "Require \"curl\" to download files" >&2
+    return 2
+  }
+
+  local CURL_OPTIONS="--fail --silent --location"
+  if [ "$(uname -s)" = "Darwin" ]
+  then
+    case $(sw_vers -productVersion) in
+      10.*)
+        CURL_OPTIONS="$CURL_OPTIONS --insecure"
+        ;;
+    esac
+  fi
+
+  echo "Getting \"$REMOTE\""
+  mkdir -p "$(dirname "$LOCAL")"
+
+  if curl $CURL_OPTIONS "$REMOTE" > "${LOCAL}.part"
+  then
+    mv -f "${LOCAL}.part" "$LOCAL"
+  else
+    rm -f "${LOCAL}.part"
+    echo "Failed to download \"$REMOTE\"" >&2
+    return 2
+  fi
+}