bin/isatool
changeset 28504 7ad7d7d6df47
parent 28503 a30b7169fdd1
child 28505 f98751bd715f
--- a/bin/isatool	Sat Oct 04 16:19:49 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-#
-# Isabelle tool starter.
-
-if [ -L "$0" ]; then
-  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
-  exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
-fi
-
-
-## settings
-
-PRG="$(basename "$0")"
-
-ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-
-
-## diagnostics
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG TOOL [ARGS ...]"
-  echo
-  echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
-  echo "  for more specific help."
-  echo
-  echo "  Available tools are:"
-  (
-    ORIG_IFS="$IFS"
-    IFS=":"
-    for DIR in $ISABELLE_TOOLS
-    do
-      cd "$DIR"
-      for T in *
-      do
-        if [ -f "$T" -a -x "$T" ]; then
-          DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
-          echo "    $T - $DESCRLINE"
-        fi
-      done
-    done
-    IFS="$ORIG_IFS"
-  )
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## args
-
-[ "$#" -lt 1 -o "$1" = "-?" ] && usage
-
-TOOLNAME="$1"
-shift
-
-
-## main
-
-ORIG_IFS="$IFS"
-IFS=":"
-for DIR in $ISABELLE_TOOLS
-do
-  TOOL="$DIR/$TOOLNAME"
-  [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
-done
-IFS="$ORIG_IFS"
-
-fail "Unknown Isabelle tool: $TOOLNAME"