--- a/Admin/download-components Wed Aug 15 13:07:24 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,139 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Florian Haftmann
-# Author: Tjark Weber
-#
-# Download and unpack Isabelle components from central component store.
-
-shopt -s -o errexit
-shopt -s -o nounset
-
-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))
-
-## directory layout
-
-: ${TMPDIR:="/tmp"}
-
-: ${ISABELLE_HOME_USER:=""}
-
-if [ -z "${ISABELLE_HOME_USER}" ]; then
- ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
- ISABELLE_TOOL="${ISABELLE_HOME}/bin/isabelle"
- ISABELLE_HOME_USER="$("${ISABELLE_TOOL}" getenv -b ISABELLE_HOME_USER)"
-fi
-
-LOCAL="${ISABELLE_HOME_USER}/contrib"
-
-## 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
- tar -xzf "${TMPDIR}/${ARCHIVE}" -C "${LOCAL}" --recursive-unlink
- 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}/"
-
-[ -e "${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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/download_components Wed Aug 15 13:43:49 2012 +0200
@@ -0,0 +1,135 @@
+#!/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