Admin/lib/Tools/download_components

Turned into Admin tool download_components.

#!/usr/bin/env bash
#
# Author: Florian Haftmann
# Author: Tjark Weber
#
# DESCRIPTION: download Isabelle components

shopt -s -o errexit
shopt -s -o nounset

## directory layout

: ${TMPDIR:="/tmp"}

LOCAL="${ISABELLE_HOME_USER}/contrib"

REMOTE="http://isabelle.in.tum.de/components"

## diagnostics

PRG="$(basename "$0")"

trap 'echo "Error in ${PRG}" >&2' ERR

function usage()
{
  cat <<EOF

Usage: ${PRG} [OPTIONS] [COMPONENTS ...]

  Options are:
    -c           Download current components (as listed in Admin/components).
    -q           Quiet (do not output diagnostic messages).
    -r           Replace components already present (default is to skip).
    -x           Exit on failed download (default is to ignore).

  Download and unpack Isabelle components from central component store
  (${REMOTE}/).

EOF
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}

## process command line

# options

DOWNLOAD_CURRENT=""
ECHO="echo"
REPLACE_EXISTING=""
EXIT_ON_FAILED_DOWNLOAD=""

function getoptions()
{
  OPTIND=1
  while getopts "cqrx" OPT
  do
    case "$OPT" in
      c)
        DOWNLOAD_CURRENT=true
        ;;
      q)
        ECHO=":"
        ;;
      r)
        REPLACE_EXISTING=true
        ;;
      x)
        EXIT_ON_FAILED_DOWNLOAD=true
        ;;
      \?)
        usage
        ;;
    esac
  done
}

getoptions "$@"
shift $(($OPTIND - 1))

## download (and unpack) components

function download()
{
  if [ -e "${LOCAL}/${COMPONENT}" -a -z "${REPLACE_EXISTING}" ]; then
    "${ECHO}" "Skipping existing component ${COMPONENT}"
  else
    "${ECHO}" "${COMPONENT}"
    ARCHIVE="${COMPONENT}.tar.gz"
    if curl -s `"${ECHO}" --no-silent` -f -o "${TMPDIR}/${ARCHIVE}" "${REMOTE}/${ARCHIVE}"; then
      if [ -n "${REPLACE_EXISTING}" ]; then
        tar -xzf "${TMPDIR}/${ARCHIVE}" -C "${LOCAL}" --recursive-unlink
      else
        tar -xzf "${TMPDIR}/${ARCHIVE}" -C "${LOCAL}"
      fi
    else
      if [ -n "${EXIT_ON_FAILED_DOWNLOAD}" ]; then
        fail "Error downloading component ${COMPONENT} (non-free?)"
      else
        "${ECHO}" "Error downloading component ${COMPONENT} (non-free?)"
      fi
    fi
  fi
}

"${ECHO}" "Unpacking components into ${LOCAL}/"

mkdir -p "${LOCAL}"

# process Admin/components
if [ -n "${DOWNLOAD_CURRENT}" ]; then
  while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
  do
    case "${REPLY}" in
      \#* | "")
        ;;
      *)
        COMPONENT="$(basename "${REPLY}")"
        download "${COMPONENT}"
        ;;
    esac
  done < "${ISABELLE_HOME}/Admin/components"
fi

# process args
for COMPONENT in "$@"
do
  download "${COMPONENT}"
done