diff -r 0cf8bc6f7084 -r 9708686dbe62 Admin/lib/Tools/download_components
--- a/Admin/lib/Tools/download_components	Fri Aug 17 11:32:20 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