GPLed;
more robust handling of spaces in args / file names;

--- a/build	Fri Sep 01 17:50:36 2000 +0200
+++ b/build	Fri Sep 01 17:54:58 2000 +0200
@@ -12,11 +12,11 @@
 
 ## settings
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 export THIS_IS_ISABELLE_BUILD=true
-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; }
 
 
@@ -101,7 +101,7 @@
   echo "                *****************************"
   echo
   echo "Please check $ISABELLE_HOME/etc/settings"
-  [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
+  [ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
   echo "to make sure that Isabelle's ML system settings and compilation options"
   echo "are appropriate."
   echo
@@ -130,8 +130,8 @@
 
 for L in $LOGICS
 do
-  DIR=$ISABELLE_HOME/src/$L
-  if [ -f $DIR/IsaMakefile ]; then
+  DIR="$ISABELLE_HOME/src/$L"
+  if [ -f "$DIR/IsaMakefile" ]; then
     MAKE_LOGICS="$MAKE_LOGICS $L"
   else
     echo "No such logic: $L"
@@ -140,12 +140,12 @@
 
 
 if [ -z "$BATCH" ]; then
-  echo " " $MAKE_LOGICS
+  echo " $MAKE_LOGICS"
   echo
   read
 else
   echo
-  echo "Isabelle build:" $MAKE_LOGICS
+  echo "Isabelle build: $MAKE_LOGICS"
   echo
   echo "ML_SYSTEM=$ML_SYSTEM"
   echo "ML_HOME=$ML_HOME"
@@ -166,10 +166,10 @@
 
 for L in $MAKE_LOGICS
 do
-  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make $TARGETS )
+  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make $TARGETS )
 done
 
 echo -n "Finished at "; date
 
-ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
+ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
 echo "$ELAPSED total elapsed time"

--- a/lib/scripts/feeder	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/feeder	Fri Sep 01 17:54:58 2000 +0200
@@ -1,14 +1,16 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # feeder - feed isabelle session
 
 
 ## diagnostics
 
-PRG=$(basename $0)
-DIR=$(dirname $0)
+PRG=$(basename "$0")
+DIR=$(dirname "$0")
 
 function usage()
 {
@@ -73,7 +75,7 @@
 
 # args
 
-[ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
+[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
 
 
 
@@ -82,4 +84,4 @@
 #set by configure
 AUTO_PERL=perl
 
-exec $AUTO_PERL -w $DIR/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"
+exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"

--- a/lib/scripts/feeder.pl	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/feeder.pl	Fri Sep 01 17:54:58 2000 +0200
@@ -1,5 +1,7 @@
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # feeder.pl - feed isabelle session
 #

--- a/lib/scripts/fixclasimp.pl	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/fixclasimp.pl	Fri Sep 01 17:54:58 2000 +0200
@@ -1,5 +1,7 @@
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # fixclasimp.pl - fix references to implicit claset and simpset
 #

--- a/lib/scripts/fixdatatype.pl	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/fixdatatype.pl	Fri Sep 01 17:54:58 2000 +0200
@@ -1,5 +1,7 @@
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # fixdatatype.pl - adapt theories and proof scripts to new datatype package
 #

--- a/lib/scripts/fixdots.pl	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/fixdots.pl	Fri Sep 01 17:54:58 2000 +0200
@@ -1,5 +1,7 @@
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # fixdots.pl - ensure that dots in formulas are followed by non-idents
 #

--- a/lib/scripts/fixgoal.pl	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/fixgoal.pl	Fri Sep 01 17:54:58 2000 +0200
@@ -1,5 +1,7 @@
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # fixgoal.pl - replace goal(w) commands by implicit versions Goal(w)
 #

--- a/lib/scripts/fixseq.pl	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/fixseq.pl	Fri Sep 01 17:54:58 2000 +0200
@@ -1,5 +1,7 @@
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # fixseq.pl - fix references to obsolete Pure/Sequence structure
 #

--- a/lib/scripts/getsettings	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/getsettings	Fri Sep 01 17:54:58 2000 +0200
@@ -1,5 +1,7 @@
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # getsettings - bash source script to augment current env.
 #
@@ -12,11 +14,11 @@
 ISABELLE_SETTINGS_PRESENT=true
 
 #normalize ISABELLE_HOME as passed by caller
-ISABELLE_HOME=$(cd $ISABELLE_HOME; echo $PWD)
+ISABELLE_HOME=$(cd "$ISABELLE_HOME"; echo "$PWD")
 
 #main executables
-ISABELLE=$ISABELLE_HOME/bin/isabelle
-ISATOOL=$ISABELLE_HOME/bin/isatool
+ISABELLE="$ISABELLE_HOME/bin/isabelle"
+ISATOOL="$ISABELLE_HOME/bin/isatool"
 
 #users tend to put strange things in here ...
 unset ENV
@@ -38,9 +40,12 @@
 }
 
 #get actual settings
-. $ISABELLE_HOME/etc/settings || exit 2
+. "$ISABELLE_HOME/etc/settings" || exit 2
 ISABELLE_SITE_SETTINGS_PRESENT=true
-[ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
+
+[ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
+  { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
+[ -f "$ISABELLE_HOME_USER/etc/settings" ] && . "$ISABELLE_HOME_USER/etc/settings"
 
 #append ML system identifier to paths
 if [ -z "$ML_PLATFORM" ]; then
@@ -49,8 +54,6 @@
   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
 fi
 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
-ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_IDENTIFIER; done)
-ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :)
 
 set +o allexport
 

--- a/lib/scripts/isa-emacs	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/isa-emacs	Fri Sep 01 17:54:58 2000 +0200
@@ -1,13 +1,15 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # Emacs Isamode interface wrapper.
 
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -71,7 +73,7 @@
 
 # args
 
-[ $# != 0 ] && usage
+[ "$#" != 0 ] && usage
 
 
 ## main
@@ -82,12 +84,12 @@
 [ "$INITFILE" = false ] && ARGS="$ARGS -q"
 
 
-ARGS="$ARGS -l $ISAMODE_HOME/elisp/isa-site.el"
+ARGS="$ARGS -l \"$ISAMODE_HOME/elisp/isa-site.el\""
 
 for FILE in "$ISABELLE_HOME/etc/isa-settings.el" \
     "$ISABELLE_HOME_USER/etc/isa-settings.el"
 do
-  [ -f "$FILE" ] && ARGS="$ARGS -l $FILE"
+  [ -f "$FILE" ] && ARGS="$ARGS -l \"$FILE\""
 done
 
 ARGS="$ARGS -f isabelle"

--- a/lib/scripts/isa-xterm	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/isa-xterm	Fri Sep 01 17:54:58 2000 +0200
@@ -1,13 +1,15 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # Simple Isabelle interface based on xterm.
 
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -102,7 +104,7 @@
 PASS="$PASS_MODE $PASS"
 
 if [ -z "$SYMBOLS" -o "$SYMBOLS" = false ]; then
-  exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e $ISABELLE $PASS "$@"
+  exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e \"$ISABELLE\" $PASS "$@"
 else
   $ISATOOL installfonts
   exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -fn isabelle14 \
@@ -119,5 +121,5 @@
     -xrm "*VT100*font5:" \
     -xrm "*fontMenu*font6*Label:" \
     -xrm "*VT100*font6:" \
-    -e $ISABELLE -m isabelle_font -m symbols $PASS "$@"
+    -e \"$ISABELLE\" -m isabelle_font -m symbols $PASS "$@"
 fi

--- a/lib/scripts/patch-scripts.bash	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/patch-scripts.bash	Fri Sep 01 17:54:58 2000 +0200
@@ -1,5 +1,7 @@
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # patch-scripts.bash - relocate interpreter paths of executable scripts and
 #   insert AUTO_BASH/AUTO_PERL values
@@ -38,14 +40,14 @@
   if [ -x "$FILE" ]; then
     sed -e "s:^#!.*/bash:#!$BASH_PATH:" -e "s:^#!.*/perl:#!$PERL_PATH:" \
       -e "s:^AUTO_BASH=.*bash:AUTO_BASH=$AUTO_BASH:" \
-      -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" $FILE >$FILE~~
-    if cmp -s $FILE $FILE~~; then
-      rm $FILE~~
+      -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~"
+    if cmp -s "$FILE" "$FILE~~"; then
+      rm "$FILE~~"
     else
-      rm -f $FILE
-      mv $FILE~~ $FILE
-      chmod +x $FILE
-      echo fixed $FILE
+      rm -f "$FILE"
+      mv "$FILE~~" "$FILE"
+      chmod +x "$FILE"
+      echo "fixed $FILE"
     fi
   fi
 done

--- a/lib/scripts/run-mlworks	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/run-mlworks	Fri Sep 01 17:54:58 2000 +0200
@@ -1,6 +1,8 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # MLWorks startup script (for 1.0r2 or later).
 #
@@ -24,7 +26,7 @@
   MLWORKS="mlworks-basis -tty"
 else
   EXIT=""
-  MLWORKS="mlimage -load $INFILE -tty"
+  MLWORKS="mlimage -load \"$INFILE\" -tty"
 fi
 
 if [ -z "$OUTFILE" ]; then
@@ -46,10 +48,10 @@
   FEEDER_OPTS="-q"
 fi
 
-$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-  { read FPID; $ML_HOME/$MLWORKS $ML_OPTIONS 2>&1; RC=$?; kill -HUP $FPID; exit $RC; }
-RC=$?
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+  { read FPID; "$ML_HOME/$MLWORKS" $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+RC="$?"
 
 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 
-exit $RC
+exit "$RC"

--- a/lib/scripts/run-mosml	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/run-mosml	Fri Sep 01 17:54:58 2000 +0200
@@ -1,6 +1,8 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # Moscow ML 2.00 startup script
 #
@@ -49,10 +51,10 @@
   FEEDER_OPTS="-q"
 fi
 
-$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-  { read FPID; $ML_HOME/$MOSML $ML_OPTIONS 2>&1; RC=$?; kill -HUP $FPID; exit $RC; }
-RC=$?
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+  { read FPID; "$ML_HOME/$MOSML" $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+RC="$?"
 
 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 
-exit $RC
+exit "$RC"

--- a/lib/scripts/run-polyml	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/run-polyml	Fri Sep 01 17:54:58 2000 +0200
@@ -1,6 +1,8 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # Poly/ML startup script.
 #
@@ -28,8 +30,8 @@
 
 ## Poly/ML programs
 
-POLY=$ML_HOME/poly
-DISCGARB=$ML_HOME/discgarb
+POLY="$ML_HOME/poly"
+DISCGARB="$ML_HOME/discgarb"
 
 check_mlhome_file "$POLY"
 check_mlhome_file "$DISCGARB"
@@ -68,7 +70,7 @@
   DB="$OUTFILE"
 else
   [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
-  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE"
+  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
   [ -f "$OUTFILE" ] || fail_out
   DB="$OUTFILE"
 fi
@@ -84,12 +86,12 @@
 
 DB_INFO=$(ls -l "$DB")
 
-$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" $FEEDER_OPTS | \
-  { read FPID; $POLY $ML_OPTIONS "$DB"; RC=$?; kill -HUP $FPID; exit $RC; }
-RC=$?
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
+  { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+RC="$?"
 
 NEW_DB_INFO=$(ls -l "$DB")
-[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB -c "$OUTFILE"
+[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && "$DISCGARB" -c "$OUTFILE"
 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 
-exit $RC
+exit "$RC"

--- a/lib/scripts/run-smlnj	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/run-smlnj	Fri Sep 01 17:54:58 2000 +0200
@@ -1,6 +1,8 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # SML/NJ startup script (for 110 or later).
 #
@@ -76,19 +78,19 @@
   FEEDER_OPTS="-q"
 fi
 
-$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-  { read FPID; $SML $ML_OPTIONS $DB; RC=$?; kill -HUP $FPID; exit $RC; }
-RC=$?
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+  { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+RC="$?"
 
 
 ## fix heap file name and permissions
 
 if [ -n "$OUTFILE" ]; then
-  eval $($ARCH_N_OPSYS)
+  eval $("$ARCH_N_OPSYS")
   [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS"
   HEAP="$OUTFILE.$HEAP_SUFFIX"
   check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \
     [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 fi
 
-exit $RC
+exit "$RC"

--- a/lib/scripts/run-smlnj-0.93	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/run-smlnj-0.93	Fri Sep 01 17:54:58 2000 +0200
@@ -1,6 +1,8 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # SML/NJ startup script (for 0.93).
 #
@@ -43,7 +45,7 @@
 else
   if [ "$INFILE" -ef "$OUTFILE" ]; then
     OUTDIR=$(dirname "$OUTFILE")/tmp
-    OUTFILE=$OUTDIR/$(basename "$OUTFILE")
+    OUTFILE="$OUTDIR"/$(basename "$OUTFILE")
     mkdir -p "$OUTDIR" || fail_out
     MOVE=true
   fi
@@ -63,9 +65,9 @@
   FEEDER_OPTS="-q"
 fi
 
-$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-  { read FPID; $INFILE $ML_OPTIONS; RC=$?; kill -HUP $FPID; exit $RC; }
-RC=$?
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+  { read FPID; "$INFILE" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
+RC="$?"
 
 
 ## fix heap file
@@ -77,4 +79,4 @@
   mv "$OUTFILE" "$INFILE" || fail_out
 fi
 
-exit $RC
+exit "$RC"

--- a/lib/scripts/showtime	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/showtime	Fri Sep 01 17:54:58 2000 +0200
@@ -1,16 +1,18 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # showtime - print time.
 
-TIME=$1
+TIME="$1"
 
 SECS=$[ $TIME % 60 ]
-[ $SECS -lt 10 ] && SECS=0$SECS
+[ $SECS -lt 10 ] && SECS="0$SECS"
 
 MINUTES=$[ ($TIME / 60) % 60 ]
-[ $MINUTES -lt 10 ] && MINUTES=0$MINUTES
+[ $MINUTES -lt 10 ] && MINUTES="0$MINUTES"
 
 HOURS=$[ $TIME / 3600 ]
 

--- a/lib/scripts/symbolinput.pl	Fri Sep 01 17:50:36 2000 +0200
+++ b/lib/scripts/symbolinput.pl	Fri Sep 01 17:54:58 2000 +0200
@@ -1,5 +1,7 @@
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # symbolinput.pl - expand isabelle-0 encoded chars to \<...> sequences.
 #

--- a/src/Pure/mk	Fri Sep 01 17:50:36 2000 +0200
+++ b/src/Pure/mk	Fri Sep 01 17:54:58 2000 +0200
@@ -1,6 +1,8 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # mk - build Pure Isabelle.
 #
@@ -51,14 +53,14 @@
 
 # args
 
-[ $# -ne 0 ] && usage
+[ "$#" -ne 0 ] && usage
 
 
 ## main
 
 # get compatibility file
 
-ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
+ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
 [ -z "$ML_SYSTEM" ] && \
   fail "Missing ML system settings! Probably not run via 'isatool make'."
 
@@ -83,35 +85,35 @@
   echo "Building $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
-  $ISABELLE \
+  "$ISABELLE" \
     -e "val ml_system = \"$ML_SYSTEM\";" \
     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
-    -c -q -w RAW_ML_SYSTEM Pure > $LOG 2>&1
-  RC=$?
+    -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
+  RC="$?"
 else
   ITEM="RAW"
   echo "Building $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
-  $ISABELLE \
+  "$ISABELLE" \
     -e "val ml_system = \"$ML_SYSTEM\";" \
     -e "use\"$COMPAT\" handle _ => exit 1;;" \
-    -q -w RAW_ML_SYSTEM RAW > $LOG 2>&1
-  RC=$?
+    -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
+  RC="$?"
 fi
 
-ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
+ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
 
 
 # exit status
 
-if [ $RC -eq 0 ]; then
+if [ "$RC" -eq 0 ]; then
   echo "Finished $ITEM ($ELAPSED elapsed time)"
   gzip --force "$LOG"
 else
   echo "$ITEM FAILED"
   echo "(see also $LOG)"
-  echo; tail $LOG; echo
+  echo; tail "$LOG"; echo
 fi
 
-exit $RC
+exit "$RC"