equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # Author: Markus Wenzel, TU Muenchen |
4 # Author: Markus Wenzel, TU Muenchen |
5 # |
5 # |
6 # Isabelle tool starter -- provides settings environment |
6 # Isabelle tool starter. |
7 # and keeps your PATH name space clean. |
|
8 |
7 |
9 if [ -L "$0" ]; then |
8 if [ -L "$0" ]; then |
10 TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" |
9 TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')" |
11 exec "$(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" |
10 exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@" |
12 fi |
11 fi |
13 |
12 |
14 |
13 |
15 ## settings |
14 ## settings |
16 |
15 |
17 PRG="$(basename "$0")" |
16 PRG="$(basename "$0")" |
18 |
17 |
19 ISABELLE_HOME="$(dirname "$0")/.." |
18 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" |
20 . "$ISABELLE_HOME/lib/scripts/getsettings" || \ |
19 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 |
21 { echo "$PRG probably not called from its original place!"; exit 2; } |
|
22 |
20 |
23 |
21 |
24 ## diagnostics |
22 ## diagnostics |
25 |
23 |
26 function usage() |
24 function usage() |
36 ORIG_IFS="$IFS" |
34 ORIG_IFS="$IFS" |
37 IFS=":" |
35 IFS=":" |
38 for DIR in $ISABELLE_TOOLS |
36 for DIR in $ISABELLE_TOOLS |
39 do |
37 do |
40 cd "$DIR" |
38 cd "$DIR" |
41 echo |
|
42 for T in * |
39 for T in * |
43 do |
40 do |
44 if [ -f "$T" -a -x "$T" ]; then |
41 if [ -f "$T" -a -x "$T" ]; then |
45 DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//') |
42 DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//') |
46 echo " $T - $DESCRLINE" |
43 echo " $T - $DESCRLINE" |
47 fi |
44 fi |
48 done |
45 done |
49 done |
46 done |
50 IFS="$ORIG_IFS" |
47 IFS="$ORIG_IFS" |
51 ) |
48 ) |
52 echo |
|
53 exit 1 |
49 exit 1 |
54 } |
50 } |
55 |
51 |
56 function fail() |
52 function fail() |
57 { |
53 { |