# HG changeset patch
# User webertj
# Date 1345031022 -7200
# Node ID 01d1734f779d4e0540eef920923168384d68cde7
# Parent  9509fc5485b2538a4f8557ce173fc69be33bf79a
Turned into Admin tool download_components.

diff -r 9509fc5485b2 -r 01d1734f779d Admin/download-components
--- 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
diff -r 9509fc5485b2 -r 01d1734f779d Admin/lib/Tools/download_components
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/download_components	Wed Aug 15 13:43:42 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