Admin/download-components
changeset 48817 01d1734f779d
parent 48812 9509fc5485b2
child 48818 20336d435682
--- a/Admin/download-components	Wed Aug 15 11:04:56 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