author | wenzelm |
Tue, 17 Nov 1998 14:10:40 +0100 | |
changeset 5911 | 7da8033264fa |
parent 3276 | f8bf5e5c1641 |
child 7971 | 023778c8a029 |
permissions | -rwxr-xr-x |
3007 | 1 |
#!/bin/bash |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
2 |
# |
2307 | 3 |
# $Id$ |
4 |
# |
|
2735
29434f9b95dd
even more robust and user friendly invocation (no longer requieres
wenzelm
parents:
2703
diff
changeset
|
5 |
# Isabelle tool starter -- provides settings environment, |
2787 | 6 |
# and keeps your PATH name space clean. |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
7 |
|
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
8 |
|
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
9 |
## settings |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
10 |
|
2703 | 11 |
PRG=$(basename $0) |
12 |
||
2735
29434f9b95dd
even more robust and user friendly invocation (no longer requieres
wenzelm
parents:
2703
diff
changeset
|
13 |
ISABELLE_HOME=$(dirname $0)/.. |
29434f9b95dd
even more robust and user friendly invocation (no longer requieres
wenzelm
parents:
2703
diff
changeset
|
14 |
. $ISABELLE_HOME/lib/scripts/getsettings || \ |
2936
bd33e7aae062
fixed { ... } shell syntax to accomodate bash 2.x;
wenzelm
parents:
2787
diff
changeset
|
15 |
{ 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
|
16 |
|
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
17 |
|
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
18 |
## diagnostics |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
19 |
|
2787 | 20 |
TOOLDIRS=$(echo $ISABELLE_TOOLS | tr : " ") |
21 |
||
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
22 |
function usage() |
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 |
echo |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
25 |
echo "Usage: $PRG TOOL [ARGS ...]" |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
26 |
echo |
2434 | 27 |
echo " Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL" |
2787 | 28 |
echo " for more specific help." |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
29 |
echo |
3276 | 30 |
echo " Available tools are:" |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
31 |
( |
2787 | 32 |
for DIR in $TOOLDIRS |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
33 |
do |
2787 | 34 |
cd $DIR |
35 |
echo |
|
36 |
for T in * |
|
37 |
do |
|
38 |
if [ -f "$T" -a -x "$T" ]; then |
|
39 |
DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//') |
|
40 |
echo " $T - $DESCRLINE" |
|
41 |
fi |
|
42 |
done |
|
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
43 |
done |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
44 |
) |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
45 |
echo |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
46 |
exit 1 |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
47 |
} |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
48 |
|
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
49 |
function fail() |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
50 |
{ |
2344 | 51 |
echo "$1" >&2 |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
52 |
exit 2 |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
53 |
} |
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 |
|
2787 | 56 |
## args |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
57 |
|
2505 | 58 |
[ $# -lt 1 -o "$1" = "-?" ] && usage |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
59 |
|
2787 | 60 |
TOOLNAME="$1" |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
61 |
shift |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
62 |
|
2787 | 63 |
|
64 |
## main |
|
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
65 |
|
2787 | 66 |
for DIR in $TOOLDIRS |
67 |
do |
|
68 |
TOOL=$DIR/$TOOLNAME |
|
69 |
[ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" |
|
70 |
done |
|
71 |
||
72 |
fail "Unknown isabelle tool: $TOOLNAME" |