equal
deleted
inserted
replaced
15 PRG="$(basename "$0")" |
15 PRG="$(basename "$0")" |
16 |
16 |
17 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" |
17 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" |
18 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 |
18 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 |
19 |
19 |
20 splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}") |
|
21 |
|
22 |
20 |
23 ## diagnostics |
21 ## diagnostics |
24 |
22 |
25 function usage() |
23 function usage() |
26 { |
24 { |
28 echo "Usage: $PRG NAME [ARGS ...]" |
26 echo "Usage: $PRG NAME [ARGS ...]" |
29 echo |
27 echo |
30 echo " Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help." |
28 echo " Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help." |
31 echo |
29 echo |
32 echo " Available tools are:" |
30 echo " Available tools are:" |
33 for DIR in "${TOOLS[@]}" |
31 perl -w "$ISABELLE_HOME/lib/scripts/tools.pl" |
34 do |
|
35 if [ -d "$DIR" ]; then |
|
36 for TOOL in "$DIR"/* |
|
37 do |
|
38 if [ -f "$TOOL" -a -x "$TOOL" ]; then |
|
39 NAME="$(basename "$TOOL")" |
|
40 DESCRLINE="$(fgrep DESCRIPTION: "$TOOL" | sed -e 's/^.*DESCRIPTION: *//')" |
|
41 echo " $NAME - $DESCRLINE" |
|
42 fi |
|
43 done |
|
44 fi |
|
45 done |
|
46 exit 1 |
32 exit 1 |
47 } |
33 } |
48 |
34 |
49 function fail() |
35 function fail() |
50 { |
36 { |
61 shift |
47 shift |
62 |
48 |
63 |
49 |
64 ## main |
50 ## main |
65 |
51 |
|
52 splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}") |
|
53 |
66 for DIR in "${TOOLS[@]}" |
54 for DIR in "${TOOLS[@]}" |
67 do |
55 do |
68 TOOL="$DIR/$TOOLNAME" |
56 TOOL="$DIR/$TOOLNAME" |
69 [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" |
57 case "$TOOL" in |
|
58 *~) ;; |
|
59 *) [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" ;; |
|
60 esac |
70 done |
61 done |
71 |
62 |
72 fail "Unknown Isabelle tool: $TOOLNAME" |
63 fail "Unknown Isabelle tool: $TOOLNAME" |