--- a/bin/isatool Fri Sep 01 17:45:07 2000 +0200
+++ b/bin/isatool Fri Sep 01 17:47:20 2000 +0200
@@ -1,24 +1,24 @@
#!/bin/bash
#
# $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
-# Isabelle tool starter -- provides settings environment,
-# and keeps your PATH name space clean.
+# Isabelle tool starter -- provides settings environment
+# and keeps your PATH name space clean.
## settings
-PRG=$(basename $0)
+PRG=$(basename "$0")
-ISABELLE_HOME=$(dirname $0)/..
-. $ISABELLE_HOME/lib/scripts/getsettings || \
+ISABELLE_HOME=$(dirname "$0")/..
+. "$ISABELLE_HOME/lib/scripts/getsettings" || \
{ echo "$PRG probably not called from its original place!"; exit 2; }
## diagnostics
-TOOLDIRS=$(echo $ISABELLE_TOOLS | tr : " ")
-
function usage()
{
echo
@@ -29,9 +29,11 @@
echo
echo " Available tools are:"
(
- for DIR in $TOOLDIRS
+ ORIG_IFS="$IFS"
+ IFS=":"
+ for DIR in $ISABELLE_TOOLS
do
- cd $DIR
+ cd "$DIR"
echo
for T in *
do
@@ -41,6 +43,7 @@
fi
done
done
+ IFS="$ORIG_IFS"
)
echo
exit 1
@@ -55,7 +58,7 @@
## args
-[ $# -lt 1 -o "$1" = "-?" ] && usage
+[ "$#" -lt 1 -o "$1" = "-?" ] && usage
TOOLNAME="$1"
shift
@@ -63,10 +66,13 @@
## main
-for DIR in $TOOLDIRS
+ORIG_IFS="$IFS"
+IFS=":"
+for DIR in $ISABELLE_TOOLS
do
- TOOL=$DIR/$TOOLNAME
+ TOOL="$DIR/$TOOLNAME"
[ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
done
+IFS="$ORIG_IFS"
fail "Unknown Isabelle tool: $TOOLNAME"