--- a/bin/isabelle Fri Sep 01 17:45:07 2000 +0200
+++ b/bin/isabelle Fri Sep 01 17:47:20 2000 +0200
@@ -1,16 +1,18 @@
#!/bin/bash
#
# $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# Basic Isabelle startup script.
## 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; }
@@ -102,17 +104,17 @@
INPUT=""
OUTPUT=""
-if [ $# -ge 1 ]; then
+if [ "$#" -ge 1 ]; then
INPUT="$1"
shift
fi
-if [ $# -ge 1 ]; then
+if [ "$#" -ge 1 ]; then
OUTPUT="$1"
shift
fi
-[ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
+[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
## check ML system
@@ -133,19 +135,22 @@
[ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
;;
*)
+ INFILE=""
ISA_PATH=""
- INFILE=""
- for DIR in $(echo $ISABELLE_PATH | tr : " ")
+
+ ORIG_IFS="$IFS"
+ IFS=":"
+ for DIR in $ISABELLE_PATH
do
- ISA_PATH="$ISA_PATH $DIR"
- [ -z "$INFILE" -a -f $DIR/$INPUT ] && INFILE=$DIR/$INPUT
+ DIR="$DIR/$ML_IDENTIFIER"
+ ISA_PATH="$ISA_PATH $DIR\n"
+ [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
done
+ IFS="$ORIG_IFS"
+
if [ -z "$INFILE" ]; then
echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
- for DIR in $ISA_PATH
- do
- echo " $DIR" >&2
- done
+ echo -ne "$ISA_PATH" >&2
exit 2
fi
;;
@@ -178,20 +183,20 @@
## run it!
-ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
+ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
-if [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ]; then
- $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
+if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
+ "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
else
- $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
+ "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
fi
-RC=$?
+RC="$?"
#Do not even think of 'rm -r'!!
-rmdir $ISABELLE_TMP
+rmdir "$ISABELLE_TMP"
-exit $RC
+exit "$RC"
--- 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"