1.1 --- a/build	Fri Sep 01 17:50:36 2000 +0200
     1.2 +++ b/build	Fri Sep 01 17:54:58 2000 +0200
     1.3 @@ -12,11 +12,11 @@
     1.4  
     1.5  ## settings
     1.6  
     1.7 -PRG=$(basename $0)
     1.8 +PRG=$(basename "$0")
     1.9  
    1.10  export THIS_IS_ISABELLE_BUILD=true
    1.11 -ISABELLE_HOME=$(dirname $0)
    1.12 -. $ISABELLE_HOME/lib/scripts/getsettings || \
    1.13 +ISABELLE_HOME=$(dirname "$0")
    1.14 +. "$ISABELLE_HOME/lib/scripts/getsettings" || \
    1.15    { echo "$PRG probably not called from its original place!"; exit 2; }
    1.16  
    1.17  
    1.18 @@ -101,7 +101,7 @@
    1.19    echo "                *****************************"
    1.20    echo
    1.21    echo "Please check $ISABELLE_HOME/etc/settings"
    1.22 -  [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
    1.23 +  [ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings"
    1.24    echo "to make sure that Isabelle's ML system settings and compilation options"
    1.25    echo "are appropriate."
    1.26    echo
    1.27 @@ -130,8 +130,8 @@
    1.28  
    1.29  for L in $LOGICS
    1.30  do
    1.31 -  DIR=$ISABELLE_HOME/src/$L
    1.32 -  if [ -f $DIR/IsaMakefile ]; then
    1.33 +  DIR="$ISABELLE_HOME/src/$L"
    1.34 +  if [ -f "$DIR/IsaMakefile" ]; then
    1.35      MAKE_LOGICS="$MAKE_LOGICS $L"
    1.36    else
    1.37      echo "No such logic: $L"
    1.38 @@ -140,12 +140,12 @@
    1.39  
    1.40  
    1.41  if [ -z "$BATCH" ]; then
    1.42 -  echo " " $MAKE_LOGICS
    1.43 +  echo " $MAKE_LOGICS"
    1.44    echo
    1.45    read
    1.46  else
    1.47    echo
    1.48 -  echo "Isabelle build:" $MAKE_LOGICS
    1.49 +  echo "Isabelle build: $MAKE_LOGICS"
    1.50    echo
    1.51    echo "ML_SYSTEM=$ML_SYSTEM"
    1.52    echo "ML_HOME=$ML_HOME"
    1.53 @@ -166,10 +166,10 @@
    1.54  
    1.55  for L in $MAKE_LOGICS
    1.56  do
    1.57 -  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make $TARGETS )
    1.58 +  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make $TARGETS )
    1.59  done
    1.60  
    1.61  echo -n "Finished at "; date
    1.62  
    1.63 -ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
    1.64 +ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
    1.65  echo "$ELAPSED total elapsed time"

     2.1 --- a/lib/scripts/feeder	Fri Sep 01 17:50:36 2000 +0200
     2.2 +++ b/lib/scripts/feeder	Fri Sep 01 17:54:58 2000 +0200
     2.3 @@ -1,14 +1,16 @@
     2.4  #!/bin/bash
     2.5  #
     2.6  # $Id$
     2.7 +# Author: Markus Wenzel, TU Muenchen
     2.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     2.9  #
    2.10  # feeder - feed isabelle session
    2.11  
    2.12  
    2.13  ## diagnostics
    2.14  
    2.15 -PRG=$(basename $0)
    2.16 -DIR=$(dirname $0)
    2.17 +PRG=$(basename "$0")
    2.18 +DIR=$(dirname "$0")
    2.19  
    2.20  function usage()
    2.21  {
    2.22 @@ -73,7 +75,7 @@
    2.23  
    2.24  # args
    2.25  
    2.26 -[ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
    2.27 +[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
    2.28  
    2.29  
    2.30  
    2.31 @@ -82,4 +84,4 @@
    2.32  #set by configure
    2.33  AUTO_PERL=perl
    2.34  
    2.35 -exec $AUTO_PERL -w $DIR/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"
    2.36 +exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"

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

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

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

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

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

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

     9.1 --- a/lib/scripts/getsettings	Fri Sep 01 17:50:36 2000 +0200
     9.2 +++ b/lib/scripts/getsettings	Fri Sep 01 17:54:58 2000 +0200
     9.3 @@ -1,5 +1,7 @@
     9.4  #
     9.5  # $Id$
     9.6 +# Author: Markus Wenzel, TU Muenchen
     9.7 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     9.8  #
     9.9  # getsettings - bash source script to augment current env.
    9.10  #
    9.11 @@ -12,11 +14,11 @@
    9.12  ISABELLE_SETTINGS_PRESENT=true
    9.13  
    9.14  #normalize ISABELLE_HOME as passed by caller
    9.15 -ISABELLE_HOME=$(cd $ISABELLE_HOME; echo $PWD)
    9.16 +ISABELLE_HOME=$(cd "$ISABELLE_HOME"; echo "$PWD")
    9.17  
    9.18  #main executables
    9.19 -ISABELLE=$ISABELLE_HOME/bin/isabelle
    9.20 -ISATOOL=$ISABELLE_HOME/bin/isatool
    9.21 +ISABELLE="$ISABELLE_HOME/bin/isabelle"
    9.22 +ISATOOL="$ISABELLE_HOME/bin/isatool"
    9.23  
    9.24  #users tend to put strange things in here ...
    9.25  unset ENV
    9.26 @@ -38,9 +40,12 @@
    9.27  }
    9.28  
    9.29  #get actual settings
    9.30 -. $ISABELLE_HOME/etc/settings || exit 2
    9.31 +. "$ISABELLE_HOME/etc/settings" || exit 2
    9.32  ISABELLE_SITE_SETTINGS_PRESENT=true
    9.33 -[ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings
    9.34 +
    9.35 +[ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \
    9.36 +  { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; }
    9.37 +[ -f "$ISABELLE_HOME_USER/etc/settings" ] && . "$ISABELLE_HOME_USER/etc/settings"
    9.38  
    9.39  #append ML system identifier to paths
    9.40  if [ -z "$ML_PLATFORM" ]; then
    9.41 @@ -49,8 +54,6 @@
    9.42    ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
    9.43  fi
    9.44  ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
    9.45 -ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_IDENTIFIER; done)
    9.46 -ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :)
    9.47  
    9.48  set +o allexport
    9.49  

    10.1 --- a/lib/scripts/isa-emacs	Fri Sep 01 17:50:36 2000 +0200
    10.2 +++ b/lib/scripts/isa-emacs	Fri Sep 01 17:54:58 2000 +0200
    10.3 @@ -1,13 +1,15 @@
    10.4  #!/bin/bash
    10.5  #
    10.6  # $Id$
    10.7 +# Author: Markus Wenzel, TU Muenchen
    10.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    10.9  #
   10.10  # Emacs Isamode interface wrapper.
   10.11  
   10.12  
   10.13  ## diagnostics
   10.14  
   10.15 -PRG=$(basename $0)
   10.16 +PRG=$(basename "$0")
   10.17  
   10.18  function usage()
   10.19  {
   10.20 @@ -71,7 +73,7 @@
   10.21  
   10.22  # args
   10.23  
   10.24 -[ $# != 0 ] && usage
   10.25 +[ "$#" != 0 ] && usage
   10.26  
   10.27  
   10.28  ## main
   10.29 @@ -82,12 +84,12 @@
   10.30  [ "$INITFILE" = false ] && ARGS="$ARGS -q"
   10.31  
   10.32  
   10.33 -ARGS="$ARGS -l $ISAMODE_HOME/elisp/isa-site.el"
   10.34 +ARGS="$ARGS -l \"$ISAMODE_HOME/elisp/isa-site.el\""
   10.35  
   10.36  for FILE in "$ISABELLE_HOME/etc/isa-settings.el" \
   10.37      "$ISABELLE_HOME_USER/etc/isa-settings.el"
   10.38  do
   10.39 -  [ -f "$FILE" ] && ARGS="$ARGS -l $FILE"
   10.40 +  [ -f "$FILE" ] && ARGS="$ARGS -l \"$FILE\""
   10.41  done
   10.42  
   10.43  ARGS="$ARGS -f isabelle"

    11.1 --- a/lib/scripts/isa-xterm	Fri Sep 01 17:50:36 2000 +0200
    11.2 +++ b/lib/scripts/isa-xterm	Fri Sep 01 17:54:58 2000 +0200
    11.3 @@ -1,13 +1,15 @@
    11.4  #!/bin/bash
    11.5  #
    11.6  # $Id$
    11.7 +# Author: Markus Wenzel, TU Muenchen
    11.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    11.9  #
   11.10  # Simple Isabelle interface based on xterm.
   11.11  
   11.12  
   11.13  ## diagnostics
   11.14  
   11.15 -PRG=$(basename $0)
   11.16 +PRG=$(basename "$0")
   11.17  
   11.18  function usage()
   11.19  {
   11.20 @@ -102,7 +104,7 @@
   11.21  PASS="$PASS_MODE $PASS"
   11.22  
   11.23  if [ -z "$SYMBOLS" -o "$SYMBOLS" = false ]; then
   11.24 -  exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e $ISABELLE $PASS "$@"
   11.25 +  exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -e \"$ISABELLE\" $PASS "$@"
   11.26  else
   11.27    $ISATOOL installfonts
   11.28    exec $XTERM -T Isabelle -n Isabelle -geometry "$MAINGEOM" -fn isabelle14 \
   11.29 @@ -119,5 +121,5 @@
   11.30      -xrm "*VT100*font5:" \
   11.31      -xrm "*fontMenu*font6*Label:" \
   11.32      -xrm "*VT100*font6:" \
   11.33 -    -e $ISABELLE -m isabelle_font -m symbols $PASS "$@"
   11.34 +    -e \"$ISABELLE\" -m isabelle_font -m symbols $PASS "$@"
   11.35  fi

    12.1 --- a/lib/scripts/patch-scripts.bash	Fri Sep 01 17:50:36 2000 +0200
    12.2 +++ b/lib/scripts/patch-scripts.bash	Fri Sep 01 17:54:58 2000 +0200
    12.3 @@ -1,5 +1,7 @@
    12.4  #
    12.5  # $Id$
    12.6 +# Author: Markus Wenzel, TU Muenchen
    12.7 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    12.8  #
    12.9  # patch-scripts.bash - relocate interpreter paths of executable scripts and
   12.10  #   insert AUTO_BASH/AUTO_PERL values
   12.11 @@ -38,14 +40,14 @@
   12.12    if [ -x "$FILE" ]; then
   12.13      sed -e "s:^#!.*/bash:#!$BASH_PATH:" -e "s:^#!.*/perl:#!$PERL_PATH:" \
   12.14        -e "s:^AUTO_BASH=.*bash:AUTO_BASH=$AUTO_BASH:" \
   12.15 -      -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" $FILE >$FILE~~
   12.16 -    if cmp -s $FILE $FILE~~; then
   12.17 -      rm $FILE~~
   12.18 +      -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~"
   12.19 +    if cmp -s "$FILE" "$FILE~~"; then
   12.20 +      rm "$FILE~~"
   12.21      else
   12.22 -      rm -f $FILE
   12.23 -      mv $FILE~~ $FILE
   12.24 -      chmod +x $FILE
   12.25 -      echo fixed $FILE
   12.26 +      rm -f "$FILE"
   12.27 +      mv "$FILE~~" "$FILE"
   12.28 +      chmod +x "$FILE"
   12.29 +      echo "fixed $FILE"
   12.30      fi
   12.31    fi
   12.32  done

    13.1 --- a/lib/scripts/run-mlworks	Fri Sep 01 17:50:36 2000 +0200
    13.2 +++ b/lib/scripts/run-mlworks	Fri Sep 01 17:54:58 2000 +0200
    13.3 @@ -1,6 +1,8 @@
    13.4  #!/bin/bash
    13.5  #
    13.6  # $Id$
    13.7 +# Author: Markus Wenzel, TU Muenchen
    13.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    13.9  #
   13.10  # MLWorks startup script (for 1.0r2 or later).
   13.11  #
   13.12 @@ -24,7 +26,7 @@
   13.13    MLWORKS="mlworks-basis -tty"
   13.14  else
   13.15    EXIT=""
   13.16 -  MLWORKS="mlimage -load $INFILE -tty"
   13.17 +  MLWORKS="mlimage -load \"$INFILE\" -tty"
   13.18  fi
   13.19  
   13.20  if [ -z "$OUTFILE" ]; then
   13.21 @@ -46,10 +48,10 @@
   13.22    FEEDER_OPTS="-q"
   13.23  fi
   13.24  
   13.25 -$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
   13.26 -  { read FPID; $ML_HOME/$MLWORKS $ML_OPTIONS 2>&1; RC=$?; kill -HUP $FPID; exit $RC; }
   13.27 -RC=$?
   13.28 +"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
   13.29 +  { read FPID; "$ML_HOME/$MLWORKS" $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
   13.30 +RC="$?"
   13.31  
   13.32  [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
   13.33  
   13.34 -exit $RC
   13.35 +exit "$RC"

    14.1 --- a/lib/scripts/run-mosml	Fri Sep 01 17:50:36 2000 +0200
    14.2 +++ b/lib/scripts/run-mosml	Fri Sep 01 17:54:58 2000 +0200
    14.3 @@ -1,6 +1,8 @@
    14.4  #!/bin/bash
    14.5  #
    14.6  # $Id$
    14.7 +# Author: Markus Wenzel, TU Muenchen
    14.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    14.9  #
   14.10  # Moscow ML 2.00 startup script
   14.11  #
   14.12 @@ -49,10 +51,10 @@
   14.13    FEEDER_OPTS="-q"
   14.14  fi
   14.15  
   14.16 -$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
   14.17 -  { read FPID; $ML_HOME/$MOSML $ML_OPTIONS 2>&1; RC=$?; kill -HUP $FPID; exit $RC; }
   14.18 -RC=$?
   14.19 +"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
   14.20 +  { read FPID; "$ML_HOME/$MOSML" $ML_OPTIONS 2>&1; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
   14.21 +RC="$?"
   14.22  
   14.23  [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
   14.24  
   14.25 -exit $RC
   14.26 +exit "$RC"

    15.1 --- a/lib/scripts/run-polyml	Fri Sep 01 17:50:36 2000 +0200
    15.2 +++ b/lib/scripts/run-polyml	Fri Sep 01 17:54:58 2000 +0200
    15.3 @@ -1,6 +1,8 @@
    15.4  #!/bin/bash
    15.5  #
    15.6  # $Id$
    15.7 +# Author: Markus Wenzel, TU Muenchen
    15.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    15.9  #
   15.10  # Poly/ML startup script.
   15.11  #
   15.12 @@ -28,8 +30,8 @@
   15.13  
   15.14  ## Poly/ML programs
   15.15  
   15.16 -POLY=$ML_HOME/poly
   15.17 -DISCGARB=$ML_HOME/discgarb
   15.18 +POLY="$ML_HOME/poly"
   15.19 +DISCGARB="$ML_HOME/discgarb"
   15.20  
   15.21  check_mlhome_file "$POLY"
   15.22  check_mlhome_file "$DISCGARB"
   15.23 @@ -68,7 +70,7 @@
   15.24    DB="$OUTFILE"
   15.25  else
   15.26    [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
   15.27 -  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE"
   15.28 +  echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE"
   15.29    [ -f "$OUTFILE" ] || fail_out
   15.30    DB="$OUTFILE"
   15.31  fi
   15.32 @@ -84,12 +86,12 @@
   15.33  
   15.34  DB_INFO=$(ls -l "$DB")
   15.35  
   15.36 -$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" $FEEDER_OPTS | \
   15.37 -  { read FPID; $POLY $ML_OPTIONS "$DB"; RC=$?; kill -HUP $FPID; exit $RC; }
   15.38 -RC=$?
   15.39 +"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \
   15.40 +  { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
   15.41 +RC="$?"
   15.42  
   15.43  NEW_DB_INFO=$(ls -l "$DB")
   15.44 -[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB -c "$OUTFILE"
   15.45 +[ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && "$DISCGARB" -c "$OUTFILE"
   15.46  [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
   15.47  
   15.48 -exit $RC
   15.49 +exit "$RC"

    16.1 --- a/lib/scripts/run-smlnj	Fri Sep 01 17:50:36 2000 +0200
    16.2 +++ b/lib/scripts/run-smlnj	Fri Sep 01 17:54:58 2000 +0200
    16.3 @@ -1,6 +1,8 @@
    16.4  #!/bin/bash
    16.5  #
    16.6  # $Id$
    16.7 +# Author: Markus Wenzel, TU Muenchen
    16.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    16.9  #
   16.10  # SML/NJ startup script (for 110 or later).
   16.11  #
   16.12 @@ -76,19 +78,19 @@
   16.13    FEEDER_OPTS="-q"
   16.14  fi
   16.15  
   16.16 -$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
   16.17 -  { read FPID; $SML $ML_OPTIONS $DB; RC=$?; kill -HUP $FPID; exit $RC; }
   16.18 -RC=$?
   16.19 +"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
   16.20 +  { read FPID; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
   16.21 +RC="$?"
   16.22  
   16.23  
   16.24  ## fix heap file name and permissions
   16.25  
   16.26  if [ -n "$OUTFILE" ]; then
   16.27 -  eval $($ARCH_N_OPSYS)
   16.28 +  eval $("$ARCH_N_OPSYS")
   16.29    [ -z "$HEAP_SUFFIX" ] && HEAP_SUFFIX="$ARCH-$OPSYS"
   16.30    HEAP="$OUTFILE.$HEAP_SUFFIX"
   16.31    check_heap_file "$HEAP" && mv "$HEAP" "$OUTFILE" && \
   16.32      [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
   16.33  fi
   16.34  
   16.35 -exit $RC
   16.36 +exit "$RC"

    17.1 --- a/lib/scripts/run-smlnj-0.93	Fri Sep 01 17:50:36 2000 +0200
    17.2 +++ b/lib/scripts/run-smlnj-0.93	Fri Sep 01 17:54:58 2000 +0200
    17.3 @@ -1,6 +1,8 @@
    17.4  #!/bin/bash
    17.5  #
    17.6  # $Id$
    17.7 +# Author: Markus Wenzel, TU Muenchen
    17.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    17.9  #
   17.10  # SML/NJ startup script (for 0.93).
   17.11  #
   17.12 @@ -43,7 +45,7 @@
   17.13  else
   17.14    if [ "$INFILE" -ef "$OUTFILE" ]; then
   17.15      OUTDIR=$(dirname "$OUTFILE")/tmp
   17.16 -    OUTFILE=$OUTDIR/$(basename "$OUTFILE")
   17.17 +    OUTFILE="$OUTDIR"/$(basename "$OUTFILE")
   17.18      mkdir -p "$OUTDIR" || fail_out
   17.19      MOVE=true
   17.20    fi
   17.21 @@ -63,9 +65,9 @@
   17.22    FEEDER_OPTS="-q"
   17.23  fi
   17.24  
   17.25 -$ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
   17.26 -  { read FPID; $INFILE $ML_OPTIONS; RC=$?; kill -HUP $FPID; exit $RC; }
   17.27 -RC=$?
   17.28 +"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
   17.29 +  { read FPID; "$INFILE" $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
   17.30 +RC="$?"
   17.31  
   17.32  
   17.33  ## fix heap file
   17.34 @@ -77,4 +79,4 @@
   17.35    mv "$OUTFILE" "$INFILE" || fail_out
   17.36  fi
   17.37  
   17.38 -exit $RC
   17.39 +exit "$RC"

    18.1 --- a/lib/scripts/showtime	Fri Sep 01 17:50:36 2000 +0200
    18.2 +++ b/lib/scripts/showtime	Fri Sep 01 17:54:58 2000 +0200
    18.3 @@ -1,16 +1,18 @@
    18.4  #!/bin/bash
    18.5  #
    18.6  # $Id$
    18.7 +# Author: Markus Wenzel, TU Muenchen
    18.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    18.9  #
   18.10  # showtime - print time.
   18.11  
   18.12 -TIME=$1
   18.13 +TIME="$1"
   18.14  
   18.15  SECS=$[ $TIME % 60 ]
   18.16 -[ $SECS -lt 10 ] && SECS=0$SECS
   18.17 +[ $SECS -lt 10 ] && SECS="0$SECS"
   18.18  
   18.19  MINUTES=$[ ($TIME / 60) % 60 ]
   18.20 -[ $MINUTES -lt 10 ] && MINUTES=0$MINUTES
   18.21 +[ $MINUTES -lt 10 ] && MINUTES="0$MINUTES"
   18.22  
   18.23  HOURS=$[ $TIME / 3600 ]
   18.24  

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

    20.1 --- a/src/Pure/mk	Fri Sep 01 17:50:36 2000 +0200
    20.2 +++ b/src/Pure/mk	Fri Sep 01 17:54:58 2000 +0200
    20.3 @@ -1,6 +1,8 @@
    20.4  #!/bin/bash
    20.5  #
    20.6  # $Id$
    20.7 +# Author: Markus Wenzel, TU Muenchen
    20.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    20.9  #
   20.10  # mk - build Pure Isabelle.
   20.11  #
   20.12 @@ -51,14 +53,14 @@
   20.13  
   20.14  # args
   20.15  
   20.16 -[ $# -ne 0 ] && usage
   20.17 +[ "$#" -ne 0 ] && usage
   20.18  
   20.19  
   20.20  ## main
   20.21  
   20.22  # get compatibility file
   20.23  
   20.24 -ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
   20.25 +ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   20.26  [ -z "$ML_SYSTEM" ] && \
   20.27    fail "Missing ML system settings! Probably not run via 'isatool make'."
   20.28  
   20.29 @@ -83,35 +85,35 @@
   20.30    echo "Building $ITEM ..."
   20.31    LOG="$LOGDIR/$ITEM"
   20.32  
   20.33 -  $ISABELLE \
   20.34 +  "$ISABELLE" \
   20.35      -e "val ml_system = \"$ML_SYSTEM\";" \
   20.36      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
   20.37 -    -c -q -w RAW_ML_SYSTEM Pure > $LOG 2>&1
   20.38 -  RC=$?
   20.39 +    -c -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
   20.40 +  RC="$?"
   20.41  else
   20.42    ITEM="RAW"
   20.43    echo "Building $ITEM ..."
   20.44    LOG="$LOGDIR/$ITEM"
   20.45  
   20.46 -  $ISABELLE \
   20.47 +  "$ISABELLE" \
   20.48      -e "val ml_system = \"$ML_SYSTEM\";" \
   20.49      -e "use\"$COMPAT\" handle _ => exit 1;;" \
   20.50 -    -q -w RAW_ML_SYSTEM RAW > $LOG 2>&1
   20.51 -  RC=$?
   20.52 +    -q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
   20.53 +  RC="$?"
   20.54  fi
   20.55  
   20.56 -ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
   20.57 +ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
   20.58  
   20.59  
   20.60  # exit status
   20.61  
   20.62 -if [ $RC -eq 0 ]; then
   20.63 +if [ "$RC" -eq 0 ]; then
   20.64    echo "Finished $ITEM ($ELAPSED elapsed time)"
   20.65    gzip --force "$LOG"
   20.66  else
   20.67    echo "$ITEM FAILED"
   20.68    echo "(see also $LOG)"
   20.69 -  echo; tail $LOG; echo
   20.70 +  echo; tail "$LOG"; echo
   20.71  fi
   20.72  
   20.73 -exit $RC
   20.74 +exit "$RC"