author | wenzelm |
Fri, 28 Feb 1997 16:55:35 +0100 | |
changeset 2703 | 5ce1310560ff |
parent 2505 | 50abca9d4043 |
child 2735 | 29434f9b95dd |
permissions | -rwxr-xr-x |
2344 | 1 |
#!/bin/bash -norc |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
2 |
# |
2307 | 3 |
# $Id$ |
4 |
# |
|
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
5 |
# Isabelle tool starter -- keeps your PATH name space clean. |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
6 |
|
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 |
## settings |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
9 |
|
2703 | 10 |
PRG=$(basename $0) |
11 |
||
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
12 |
ISABELLE_HOME=$(dirname $(dirname $0)) |
2703 | 13 |
case "$ISABELLE_HOME" in |
14 |
/*) |
|
15 |
if [ -f $ISABELLE_HOME/lib/scripts/getsettings ]; then |
|
16 |
. $ISABELLE_HOME/lib/scripts/getsettings || exit 2 |
|
17 |
else |
|
18 |
echo "ERROR: $PRG probably not called from its original place!" |
|
19 |
exit 1 |
|
20 |
fi |
|
21 |
;; |
|
22 |
*) |
|
23 |
echo "ERROR: $PRG not called with absolute path specification!" |
|
24 |
exit 1 |
|
25 |
;; |
|
26 |
esac |
|
2293
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 |
|
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
29 |
## diagnostics |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
30 |
|
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
31 |
function usage() |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
32 |
{ |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
33 |
echo |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
34 |
echo "Usage: $PRG TOOL [ARGS ...]" |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
35 |
echo |
2434 | 36 |
echo " Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL" |
37 |
echo " for specific help." |
|
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
38 |
echo |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
39 |
echo " Availabe tools are:" |
2434 | 40 |
echo |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
41 |
( |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
42 |
cd "$ISABELLE_HOME/lib/Tools" |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
43 |
for T in * |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
44 |
do |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
45 |
if [ -f "$T" -a -x "$T" ]; then |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
46 |
DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//') |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
47 |
echo " $T - $DESCRLINE" |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
48 |
fi |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
49 |
done |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
50 |
) |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
51 |
echo |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
52 |
exit 1 |
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 |
function fail() |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
56 |
{ |
2344 | 57 |
echo "$1" >&2 |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
58 |
exit 2 |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
59 |
} |
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 |
## main |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
63 |
|
2505 | 64 |
[ $# -lt 1 -o "$1" = "-?" ] && usage |
2293
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
65 |
|
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
66 |
TOOL_BASE="$1" |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
67 |
TOOL="$ISABELLE_HOME/lib/Tools/$1" |
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 |
|
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
70 |
[ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" |
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
71 |
|
749757db3ead
isatool: Isabelle tool starter -- keeps your PATH name space clean.
wenzelm
parents:
diff
changeset
|
72 |
fail "Tool not found: $TOOL_BASE" |