author | wenzelm |
Thu, 15 Apr 2004 20:32:33 +0200 | |
changeset 14572 | 1408d312d3a9 |
parent 11044 | 5873a05b4d21 |
child 14981 | e73f8140af78 |
permissions | -rwxr-xr-x |
wenzelm@10555 | 1 |
#!/usr/bin/env bash |
wenzelm@2293 | 2 |
# |
wenzelm@2307 | 3 |
# $Id$ |
wenzelm@9786 | 4 |
# Author: Markus Wenzel, TU Muenchen |
wenzelm@9786 | 5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
wenzelm@2307 | 6 |
# |
wenzelm@9786 | 7 |
# Isabelle tool starter -- provides settings environment |
wenzelm@9786 | 8 |
# and keeps your PATH name space clean. |
wenzelm@2293 | 9 |
|
wenzelm@2293 | 10 |
|
wenzelm@2293 | 11 |
## settings |
wenzelm@2293 | 12 |
|
wenzelm@10511 | 13 |
PRG="$(basename "$0")" |
wenzelm@2703 | 14 |
|
wenzelm@10511 | 15 |
ISABELLE_HOME="$(dirname "$0")/.." |
wenzelm@9786 | 16 |
. "$ISABELLE_HOME/lib/scripts/getsettings" || \ |
wenzelm@2936 | 17 |
{ echo "$PRG probably not called from its original place!"; exit 2; } |
wenzelm@2293 | 18 |
|
wenzelm@2293 | 19 |
|
wenzelm@2293 | 20 |
## diagnostics |
wenzelm@2293 | 21 |
|
wenzelm@2293 | 22 |
function usage() |
wenzelm@2293 | 23 |
{ |
wenzelm@2293 | 24 |
echo |
wenzelm@2293 | 25 |
echo "Usage: $PRG TOOL [ARGS ...]" |
wenzelm@2293 | 26 |
echo |
wenzelm@2434 | 27 |
echo " Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL" |
wenzelm@2787 | 28 |
echo " for more specific help." |
wenzelm@2293 | 29 |
echo |
wenzelm@3276 | 30 |
echo " Available tools are:" |
wenzelm@2293 | 31 |
( |
wenzelm@9786 | 32 |
ORIG_IFS="$IFS" |
wenzelm@9786 | 33 |
IFS=":" |
wenzelm@9786 | 34 |
for DIR in $ISABELLE_TOOLS |
wenzelm@2293 | 35 |
do |
wenzelm@9786 | 36 |
cd "$DIR" |
wenzelm@2787 | 37 |
echo |
wenzelm@2787 | 38 |
for T in * |
wenzelm@2787 | 39 |
do |
wenzelm@2787 | 40 |
if [ -f "$T" -a -x "$T" ]; then |
wenzelm@11044 | 41 |
DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//') |
wenzelm@2787 | 42 |
echo " $T - $DESCRLINE" |
wenzelm@2787 | 43 |
fi |
wenzelm@2787 | 44 |
done |
wenzelm@2293 | 45 |
done |
wenzelm@9786 | 46 |
IFS="$ORIG_IFS" |
wenzelm@2293 | 47 |
) |
wenzelm@2293 | 48 |
echo |
wenzelm@2293 | 49 |
exit 1 |
wenzelm@2293 | 50 |
} |
wenzelm@2293 | 51 |
|
wenzelm@2293 | 52 |
function fail() |
wenzelm@2293 | 53 |
{ |
wenzelm@2344 | 54 |
echo "$1" >&2 |
wenzelm@2293 | 55 |
exit 2 |
wenzelm@2293 | 56 |
} |
wenzelm@2293 | 57 |
|
wenzelm@2293 | 58 |
|
wenzelm@2787 | 59 |
## args |
wenzelm@2293 | 60 |
|
wenzelm@9786 | 61 |
[ "$#" -lt 1 -o "$1" = "-?" ] && usage |
wenzelm@2293 | 62 |
|
wenzelm@2787 | 63 |
TOOLNAME="$1" |
wenzelm@2293 | 64 |
shift |
wenzelm@2293 | 65 |
|
wenzelm@2293 | 66 |
|
wenzelm@2787 | 67 |
## main |
wenzelm@2787 | 68 |
|
wenzelm@9786 | 69 |
ORIG_IFS="$IFS" |
wenzelm@9786 | 70 |
IFS=":" |
wenzelm@9786 | 71 |
for DIR in $ISABELLE_TOOLS |
wenzelm@2787 | 72 |
do |
wenzelm@9786 | 73 |
TOOL="$DIR/$TOOLNAME" |
wenzelm@2787 | 74 |
[ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" |
wenzelm@2787 | 75 |
done |
wenzelm@9786 | 76 |
IFS="$ORIG_IFS" |
wenzelm@2787 | 77 |
|
wenzelm@7971 | 78 |
fail "Unknown Isabelle tool: $TOOLNAME" |