--- a/bin/isabelle Tue Aug 04 13:35:33 2009 +0200
+++ b/bin/isabelle Tue Aug 04 15:05:34 2009 +0200
@@ -17,6 +17,8 @@
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+ORIG_IFS="$IFS"; IFS=":"; declare -a TOOLS=($ISABELLE_TOOLS); IFS="$ORIG_IFS"
+
## diagnostics
@@ -28,24 +30,19 @@
echo " Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
echo
echo " Available tools are:"
- (
- ORIG_IFS="$IFS"
- IFS=":"
- for DIR in $ISABELLE_TOOLS
- do
- if [ -d "$DIR" ]; then
- cd "$DIR"
- for T in *
- do
- if [ -f "$T" -a -x "$T" ]; then
- DESCRLINE=$(fgrep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
- echo " $T - $DESCRLINE"
- fi
- done
- fi
- done
- IFS="$ORIG_IFS"
- )
+ for DIR in ${TOOLS[@]}
+ do
+ if [ -d "$DIR" ]; then
+ for TOOL in "$DIR"/*
+ do
+ if [ -f "$TOOL" -a -x "$TOOL" ]; then
+ NAME="$(basename "$TOOL")"
+ DESCRLINE="$(fgrep DESCRIPTION: "$TOOL" | sed -e 's/^.*DESCRIPTION: *//')"
+ echo " $NAME - $DESCRLINE"
+ fi
+ done
+ fi
+ done
exit 1
}
@@ -66,13 +63,10 @@
## main
-ORIG_IFS="$IFS"
-IFS=":"
-for DIR in $ISABELLE_TOOLS
+for DIR in "${TOOLS[@]}"
do
TOOL="$DIR/$TOOLNAME"
[ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
done
-IFS="$ORIG_IFS"
fail "Unknown Isabelle tool: $TOOLNAME"
--- a/bin/isabelle-process Tue Aug 04 13:35:33 2009 +0200
+++ b/bin/isabelle-process Tue Aug 04 15:05:34 2009 +0200
@@ -160,15 +160,13 @@
INFILE=""
ISA_PATH=""
- ORIG_IFS="$IFS"
- IFS=":"
- for DIR in $ISABELLE_PATH
+ ORIG_IFS="$IFS"; IFS=":"; declare -a PATHS=($ISABELLE_PATH); IFS="$ORIG_IFS"
+ for DIR in "${PATHS[@]}"
do
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
--- a/lib/Tools/doc Tue Aug 04 13:35:33 2009 +0200
+++ b/lib/Tools/doc Tue Aug 04 15:05:34 2009 +0200
@@ -34,28 +34,23 @@
## main
+ORIG_IFS="$IFS"; IFS=":"; declare -a DOCS=($ISABELLE_DOCS); IFS="$ORIG_IFS"
+
if [ -z "$DOC" ]; then
- ORIG_IFS="$IFS"
- IFS=":"
- for DIR in $ISABELLE_DOCS
+ for DIR in "${DOCS[@]}"
do
[ -d "$DIR" ] || fail "Bad document directory: $DIR"
[ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
done
- IFS="$ORIG_IFS"
else
- ORIG_IFS="$IFS"
- IFS=":"
- for DIR in $ISABELLE_DOCS
+ for DIR in "${DOCS[@]}"
do
- IFS="$ORIG_IFS"
[ -d "$DIR" ] || fail "Bad document directory: $DIR"
for FMT in "$ISABELLE_DOC_FORMAT" dvi
do
[ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
done
done
- IFS="$ORIG_IFS"
fail "Unknown Isabelle document: $DOC"
fi
--- a/lib/Tools/document Tue Aug 04 13:35:33 2009 +0200
+++ b/lib/Tools/document Tue Aug 04 15:05:34 2009 +0200
@@ -38,7 +38,7 @@
CLEAN=""
NAME="document"
OUTFORMAT=dvi
-TAGS=""
+declare -a TAGS=()
while getopts "cn:o:t:" OPT
do
@@ -53,7 +53,7 @@
OUTFORMAT="$OPTARG"
;;
t)
- TAGS="$OPTARG"
+ ORIG_IFS="$IFS"; IFS=","; TAGS=($OPTARG); IFS="$ORIG_IFS"
;;
\?)
usage
@@ -90,21 +90,20 @@
function prep_tags ()
{
(
- IFS=","
- for TAG in $TAGS
+ for TAG in "${TAGS[@]}"
do
case "$TAG" in
/*)
- echo "\\isafoldtag{${TAG:1}}"
+ echo "\\isafoldtag{${TAG:1}}"
;;
-*)
- echo "\\isadroptag{${TAG:1}}"
+ echo "\\isadroptag{${TAG:1}}"
;;
+*)
- echo "\\isakeeptag{${TAG:1}}"
+ echo "\\isakeeptag{${TAG:1}}"
;;
*)
- echo "\\isakeeptag{${TAG}}"
+ echo "\\isakeeptag{${TAG}}"
;;
esac
done
--- a/lib/Tools/findlogics Tue Aug 04 13:35:33 2009 +0200
+++ b/lib/Tools/findlogics Tue Aug 04 15:05:34 2009 +0200
@@ -22,22 +22,21 @@
[ "$#" -ne 0 ] && usage
-
-LOGICS=""
+declare -a LOGICS=()
+declare -a ISABELLE_PATHS=()
-ORIG_IFS="$IFS"
-IFS=":"
-for DIR in $ISABELLE_PATH
+ORIG_IFS="$IFS"; IFS=":"; ISABELLE_PATHS=($ISABELLE_PATH); IFS=$ORIG_IFS
+
+for DIR in "${ISABELLE_PATHS[@]}"
do
DIR="$DIR/$ML_IDENTIFIER"
for FILE in "$DIR"/*
do
if [ -f "$FILE" ]; then
NAME=$(basename "$FILE")
- LOGICS="$LOGICS $NAME"
+ LOGICS+=("$NAME")
fi
done
done
-IFS="$ORIG_IFS"
-echo $({ for L in $LOGICS; do echo "$L"; done; } | sort | uniq)
+echo $({ for L in ${LOGICS[@]}; do echo "$L"; done; } | sort | uniq)