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