--- a/Admin/lib/Tools/download_components Fri Aug 17 17:35:07 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-#!/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