# HG changeset patch
# User wenzelm
# Date 1345208197 -7200
# Node ID 7e19dc018db9af8c6e9e3df4de1c821b11076890
# Parent  f49745d1395a4d686f8f80a8875c69a229ceff0c
added "isabelle components" tool;

diff -r f49745d1395a -r 7e19dc018db9 etc/settings
--- a/etc/settings	Fri Aug 17 14:55:46 2012 +0200
+++ b/etc/settings	Fri Aug 17 14:56:37 2012 +0200
@@ -96,6 +96,8 @@
 ### Misc path settings
 ###
 
+ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
+
 # The place for user configuration, heap files, etc.
 if [ -z "$ISABELLE_IDENTIFIER" ]; then
   ISABELLE_HOME_USER="$USER_HOME/.isabelle"
diff -r f49745d1395a -r 7e19dc018db9 lib/Tools/components
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/components	Fri Aug 17 14:56:37 2012 +0200
@@ -0,0 +1,120 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: resolve Isabelle components
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [OPTIONS] [COMPONENTS ...]"
+  echo
+  echo "  Options are:"
+  echo "    -R URL       component repository (default \$ISABELLE_COMPONENT_REPOSITORY)"
+  echo "    -a           all missing components"
+  echo "    -l           list status"
+  echo
+  echo "  Resolve Isabelle components via download and installation."
+  echo "  COMPONENTS are identified via base name."
+  echo
+  echo "  ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+#options
+
+COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
+ALL_MISSING=""
+LIST_ONLY=""
+
+while getopts "R:al" OPT
+do
+  case "$OPT" in
+    R)
+      COMPONENT_REPOSITORY="$OPTARG"
+      ;;
+    a)
+      ALL_MISSING="true"
+      ;;
+    l)
+      LIST_ONLY="true"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -eq 0 -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage
+
+if [ -z "$ALL_MISSING" ]; then
+  splitarray ":" "$@"
+else
+  splitarray ":" "$ISABELLE_COMPONENTS_MISSING" "$@"
+fi
+declare -a SELECTED_COMPONENTS=("${SPLITARRAY[@]}")
+
+
+## main
+
+splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}")
+splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}")
+
+if [ -n "$LIST_ONLY" ]; then
+  echo
+  echo "Available components:"
+  for NAME in "${AVAILABLE_COMPONENTS[@]}"; do echo "  $NAME"; done
+  echo
+  echo "Missing components:"
+  for NAME in "${MISSING_COMPONENTS[@]}"; do echo "  $NAME"; done
+else
+  for NAME in "${SELECTED_COMPONENTS[@]}"
+  do
+    BASE_NAME="$(basename "$NAME")"
+    FULL_NAME=""
+    for X in "${AVAILABLE_COMPONENTS[@]}" "${MISSING_COMPONENTS[@]}"
+    do
+      [ -z "$FULL_NAME" -a "$BASE_NAME" = "$(basename "$X")" ] && FULL_NAME="$X"
+    done
+    if [ -z "$FULL_NAME" ]; then
+      echo "Ignoring irrelevant component \"$NAME\""
+    elif [ -d "$FULL_NAME" ]; then
+      echo "Skipping existing component \"$FULL_NAME\""
+    else
+      if [ ! -e "${FULL_NAME}.tar.gz" ]; then
+        REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
+        echo "Getting \"$REMOTE\""
+        perl -MLWP::Simple -e "getprint '$REMOTE';" > "${FULL_NAME}.tar.gz"
+        if perl -e "exit((stat('${FULL_NAME}.tar.gz'))[7] == 0 ? 0 : 1);"
+        then
+          rm -f "${FULL_NAME}.tar.gz"
+        fi
+      fi
+      if [ -e "${FULL_NAME}.tar.gz" ]; then
+        echo "Unpacking \"${FULL_NAME}.tar.gz\""
+        tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz"
+      fi
+    fi
+  done
+fi
+