GPLed;
authorwenzelm
Fri Sep 01 17:50:36 2000 +0200 (2000-09-01)
changeset 9788df671fa2562a
parent 9787 fb8c5a66dbe8
child 9789 7e5e6c47c0b5
GPLed;
more robust handling of spaces in args / file names;
lib/Tools/browser
lib/Tools/doc
lib/Tools/document
lib/Tools/expandshort
lib/Tools/findlogics
lib/Tools/fixclasimp
lib/Tools/fixdatatype
lib/Tools/fixdots
lib/Tools/fixgoal
lib/Tools/fixseq
lib/Tools/getenv
lib/Tools/install
lib/Tools/installfonts
lib/Tools/latex
lib/Tools/logo
lib/Tools/make
lib/Tools/makeall
lib/Tools/mkdir
lib/Tools/nonascii
lib/Tools/symbolinput
lib/Tools/usedir
     1.1 --- a/lib/Tools/browser	Fri Sep 01 17:48:31 2000 +0200
     1.2 +++ b/lib/Tools/browser	Fri Sep 01 17:50:36 2000 +0200
     1.3 @@ -1,11 +1,13 @@
     1.4  #!/bin/bash
     1.5  #
     1.6  # $Id$
     1.7 +# Author: Markus Wenzel, TU Muenchen
     1.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  #
    1.10  # DESCRIPTION: Isabelle graph browser
    1.11  
    1.12  
    1.13 -PRG=$(basename $0)
    1.14 +PRG=$(basename "$0")
    1.15  
    1.16  function usage()
    1.17  {
    1.18 @@ -42,14 +44,14 @@
    1.19  # args
    1.20  
    1.21  GRAPHFILE=""
    1.22 -[ $# -gt 0 ] && { GRAPHFILE="$1"; shift; }
    1.23 -[ $# -ne 0 ] && usage
    1.24 +[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
    1.25 +[ "$#" -ne 0 ] && usage
    1.26  
    1.27  
    1.28  ## main
    1.29  
    1.30 -export CLASSPATH=$ISABELLE_HOME/lib/browser
    1.31 -[ -z "$GRAPHFILE" ] && cd $ISABELLE_BROWSER_INFO
    1.32 +export CLASSPATH="$ISABELLE_HOME/lib/browser"
    1.33 +[ -z "$GRAPHFILE" ] && cd "$ISABELLE_BROWSER_INFO"
    1.34  
    1.35 -java GraphBrowser.GraphBrowser $GRAPHFILE
    1.36 +java GraphBrowser.GraphBrowser "$GRAPHFILE"
    1.37  [ -n "$GRAPHFILE" -a -n "$DELETE" ] && rm -f "$GRAPHFILE"
     2.1 --- a/lib/Tools/doc	Fri Sep 01 17:48:31 2000 +0200
     2.2 +++ b/lib/Tools/doc	Fri Sep 01 17:50:36 2000 +0200
     2.3 @@ -1,11 +1,13 @@
     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  # DESCRIPTION: view Isabelle documentation
    2.11  
    2.12  
    2.13 -PRG=$(basename $0)
    2.14 +PRG=$(basename "$0")
    2.15  
    2.16  function usage()
    2.17  {
    2.18 @@ -27,24 +29,28 @@
    2.19  ## args
    2.20  
    2.21  DOC=""
    2.22 -[ $# -ge 1 ] && { DOC="$1"; shift; }
    2.23 +[ "$#" -ge 1 ] && { DOC="$1"; shift; }
    2.24  
    2.25 -[ $# -ne 0 -o "$DOC" = "-?" ] && usage
    2.26 +[ "$#" -ne 0 -o "$DOC" = "-?" ] && usage
    2.27  
    2.28  
    2.29  ## main
    2.30  
    2.31 -DOCS=$(echo $ISABELLE_DOCS | tr : " ")
    2.32 -
    2.33  if [ -z "$DOC" ]; then
    2.34 -  for DIR in $DOCS
    2.35 +  ORIG_IFS="$IFS"
    2.36 +  IFS=":"
    2.37 +  for DIR in $ISABELLE_DOCS
    2.38    do
    2.39 -    [ -f $DIR/Contents ] && grep -v "^>>" $DIR/Contents
    2.40 +    [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
    2.41    done
    2.42 +  IFS="$ORIG_IFS"
    2.43  else
    2.44 -  for DIR in $DOCS
    2.45 +  ORIG_IFS="$IFS"
    2.46 +  IFS=":"
    2.47 +  for DIR in $ISABELLE_DOCS
    2.48    do
    2.49 -    [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
    2.50 +    [ -f "$DIR/$DOC.dvi" ] && { cd "$DIR"; IFS="$ORIG_IFS"; exec $DVI_VIEWER "$DOC.dvi"; }
    2.51    done
    2.52 +  IFS="$ORIG_IFS"
    2.53    fail "Unknown Isabelle document: $DOC"  
    2.54  fi
     3.1 --- a/lib/Tools/document	Fri Sep 01 17:48:31 2000 +0200
     3.2 +++ b/lib/Tools/document	Fri Sep 01 17:50:36 2000 +0200
     3.3 @@ -1,11 +1,13 @@
     3.4  #!/bin/bash
     3.5  #
     3.6  # $Id$
     3.7 +# Author: Markus Wenzel, TU Muenchen
     3.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     3.9  #
    3.10  # DESCRIPTION: prepare theory session document
    3.11  
    3.12  
    3.13 -PRG=$(basename $0)
    3.14 +PRG=$(basename "$0")
    3.15  
    3.16  function usage()
    3.17  {
    3.18 @@ -58,9 +60,9 @@
    3.19  # args
    3.20  
    3.21  DIR="document"
    3.22 -[ $# -ge 1 ] && { DIR="$1"; shift; }
    3.23 +[ "$#" -ge 1 ] && { DIR="$1"; shift; }
    3.24  
    3.25 -[ $# -ne 0 ] && usage
    3.26 +[ "$#" -ne 0 ] && usage
    3.27  
    3.28  
    3.29  ## main
    3.30 @@ -84,11 +86,11 @@
    3.31    [ -n "$CLEAN" ] && rm -f *.aux *.out
    3.32    if [ -f root.bib ]
    3.33    then
    3.34 -    $ISATOOL latex -o "$FMT" && \
    3.35 -    $ISATOOL latex -o bbl && \
    3.36 -    $ISATOOL latex -o "$FMT"
    3.37 +    "$ISATOOL" latex -o "$FMT" && \
    3.38 +    "$ISATOOL" latex -o bbl && \
    3.39 +    "$ISATOOL" latex -o "$FMT"
    3.40    else
    3.41 -    $ISATOOL latex -o "$FMT"
    3.42 +    "$ISATOOL" latex -o "$FMT"
    3.43    fi
    3.44  }
    3.45  
    3.46 @@ -98,20 +100,20 @@
    3.47    [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT"
    3.48  
    3.49    if [ -f IsaMakefile ]; then
    3.50 -    $ISATOOL make "$OUTFORMAT"
    3.51 -    RC=$?
    3.52 +    "$ISATOOL" make "$OUTFORMAT"
    3.53 +    RC="$?"
    3.54    elif [ "$OUTFORMAT" = pdf ]; then
    3.55      pre_latex pdf && \
    3.56 -    $ISATOOL latex -o pdf && \
    3.57 +    "$ISATOOL" latex -o pdf && \
    3.58      { if [ -n "$ISABELLE_THUMBPDF" ]; then
    3.59 -        $ISATOOL latex -o png && \
    3.60 -        $ISATOOL latex -o pdf
    3.61 +        "$ISATOOL" latex -o png && \
    3.62 +        "$ISATOOL" latex -o pdf
    3.63        fi; }
    3.64 -    RC=$?
    3.65 +    RC="$?"
    3.66    else
    3.67      pre_latex dvi && \
    3.68 -    $ISATOOL latex -o "$OUTFORMAT"
    3.69 -    RC=$?
    3.70 +    "$ISATOOL" latex -o "$OUTFORMAT"
    3.71 +    RC="$?"
    3.72    fi
    3.73  
    3.74    [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
    3.75 @@ -119,7 +121,7 @@
    3.76  
    3.77    exit "$RC"
    3.78  )
    3.79 -RC=$?
    3.80 +RC="$?"
    3.81  
    3.82  
    3.83  # install
     4.1 --- a/lib/Tools/expandshort	Fri Sep 01 17:48:31 2000 +0200
     4.2 +++ b/lib/Tools/expandshort	Fri Sep 01 17:50:36 2000 +0200
     4.3 @@ -1,11 +1,13 @@
     4.4  #!/bin/bash
     4.5  #
     4.6  # $Id$
     4.7 +# Author: Markus Wenzel, TU Muenchen
     4.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     4.9  #
    4.10  # DESCRIPTION: expand shorthand goal commands
    4.11  
    4.12  
    4.13 -PRG=$(basename $0)
    4.14 +PRG=$(basename "$0")
    4.15  
    4.16  function usage()
    4.17  {
    4.18 @@ -25,9 +27,9 @@
    4.19  
    4.20  ## process command line
    4.21  
    4.22 -[ $# -eq 0 -o "$1" = "-?" ] && usage
    4.23 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    4.24  
    4.25 -SPECS="$@"; shift $#
    4.26 +SPECS="$@"; shift "$#"
    4.27  
    4.28  
    4.29  ## main
    4.30 @@ -35,4 +37,4 @@
    4.31  #set by configure
    4.32  AUTO_PERL=perl
    4.33  
    4.34 -find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/expandshort.pl
    4.35 +find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/expandshort.pl"
     5.1 --- a/lib/Tools/findlogics	Fri Sep 01 17:48:31 2000 +0200
     5.2 +++ b/lib/Tools/findlogics	Fri Sep 01 17:50:36 2000 +0200
     5.3 @@ -1,11 +1,13 @@
     5.4  #!/bin/bash
     5.5  #
     5.6  # $Id$
     5.7 +# Author: Markus Wenzel, TU Muenchen
     5.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     5.9  #
    5.10  # DESCRIPTION: collect heap names from ISABELLE_PATH
    5.11  
    5.12  
    5.13 -PRG=$(basename $0)
    5.14 +PRG=$(basename "$0")
    5.15  
    5.16  function usage()
    5.17  {
    5.18 @@ -20,14 +22,17 @@
    5.19  
    5.20  ## main
    5.21  
    5.22 -[ $# -ne 0 ] && usage
    5.23 +[ "$#" -ne 0 ] && usage
    5.24  
    5.25  
    5.26  LOGICS=""
    5.27  
    5.28 -for DIR in $(echo $ISABELLE_PATH | tr : " ")
    5.29 +ORIG_IFS="$IFS"
    5.30 +IFS=":"
    5.31 +for DIR in $ISABELLE_PATH
    5.32  do
    5.33 -  for FILE in $DIR/*
    5.34 +  DIR="$DIR/$ML_IDENTIFIER"
    5.35 +  for FILE in "$DIR"/*
    5.36    do
    5.37      if [ -f "$FILE" ]; then
    5.38        NAME=$(basename "$FILE")
    5.39 @@ -35,5 +40,6 @@
    5.40      fi
    5.41    done
    5.42  done
    5.43 +IFS="$ORIG_IFS"
    5.44  
    5.45 -echo $({ for L in $LOGICS; do echo $L; done; } | sort | uniq)
    5.46 +echo $({ for L in $LOGICS; do echo "$L"; done; } | sort | uniq)
     6.1 --- a/lib/Tools/fixclasimp	Fri Sep 01 17:48:31 2000 +0200
     6.2 +++ b/lib/Tools/fixclasimp	Fri Sep 01 17:50:36 2000 +0200
     6.3 @@ -1,13 +1,15 @@
     6.4  #!/bin/bash
     6.5  #
     6.6  # $Id$
     6.7 +# Author: Markus Wenzel, TU Muenchen
     6.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     6.9  #
    6.10  # DESCRIPTION: fix references to implicit claset and simpset
    6.11  
    6.12  
    6.13  ## diagnostics
    6.14  
    6.15 -PRG=$(basename $0)
    6.16 +PRG=$(basename "$0")
    6.17  
    6.18  function usage()
    6.19  {
    6.20 @@ -25,9 +27,9 @@
    6.21  
    6.22  ## process command line
    6.23  
    6.24 -[ $# -eq 0 -o "$1" = "-?" ] && usage
    6.25 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    6.26  
    6.27 -SPECS="$@"; shift $#
    6.28 +SPECS="$@"; shift "$#"
    6.29  
    6.30  
    6.31  ## main
    6.32 @@ -35,4 +37,4 @@
    6.33  #set by configure
    6.34  AUTO_PERL=perl
    6.35  
    6.36 -find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixclasimp.pl
    6.37 +find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixclasimp.pl"
     7.1 --- a/lib/Tools/fixdatatype	Fri Sep 01 17:48:31 2000 +0200
     7.2 +++ b/lib/Tools/fixdatatype	Fri Sep 01 17:50:36 2000 +0200
     7.3 @@ -1,13 +1,15 @@
     7.4  #!/bin/bash
     7.5  #
     7.6  # $Id$
     7.7 +# Author: Markus Wenzel, TU Muenchen
     7.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     7.9  #
    7.10  # DESCRIPTION: adapt theories and proof scripts to new datatype package
    7.11  
    7.12  
    7.13  ## diagnostics
    7.14  
    7.15 -PRG=$(basename $0)
    7.16 +PRG=$(basename "$0")
    7.17  
    7.18  function usage()
    7.19  {
    7.20 @@ -25,9 +27,9 @@
    7.21  
    7.22  ## process command line
    7.23  
    7.24 -[ $# -eq 0 -o "$1" = "-?" ] && usage
    7.25 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    7.26  
    7.27 -SPECS="$@"; shift $#
    7.28 +SPECS="$@"; shift "$#"
    7.29  
    7.30  
    7.31  ## main
    7.32 @@ -36,4 +38,4 @@
    7.33  AUTO_PERL=perl
    7.34  
    7.35  find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
    7.36 -  xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixdatatype.pl
    7.37 +  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixdatatype.pl"
     8.1 --- a/lib/Tools/fixdots	Fri Sep 01 17:48:31 2000 +0200
     8.2 +++ b/lib/Tools/fixdots	Fri Sep 01 17:50:36 2000 +0200
     8.3 @@ -1,13 +1,15 @@
     8.4  #!/bin/bash
     8.5  #
     8.6  # $Id$
     8.7 +# Author: Markus Wenzel, TU Muenchen
     8.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     8.9  #
    8.10  # DESCRIPTION: ensure that dots in formulas are followed by non-idents
    8.11  
    8.12  
    8.13  ## diagnostics
    8.14  
    8.15 -PRG=$(basename $0)
    8.16 +PRG=$(basename "$0")
    8.17  
    8.18  function usage()
    8.19  {
    8.20 @@ -25,9 +27,9 @@
    8.21  
    8.22  ## process command line
    8.23  
    8.24 -[ $# -eq 0 -o "$1" = "-?" ] && usage
    8.25 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    8.26  
    8.27 -SPECS="$@"; shift $#
    8.28 +SPECS="$@"; shift "$#"
    8.29  
    8.30  
    8.31  ## main
    8.32 @@ -36,4 +38,4 @@
    8.33  AUTO_PERL=perl
    8.34  
    8.35  find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
    8.36 -  xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixdots.pl
    8.37 +  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixdots.pl"
     9.1 --- a/lib/Tools/fixgoal	Fri Sep 01 17:48:31 2000 +0200
     9.2 +++ b/lib/Tools/fixgoal	Fri Sep 01 17:50:36 2000 +0200
     9.3 @@ -1,13 +1,15 @@
     9.4  #!/bin/bash
     9.5  #
     9.6  # $Id$
     9.7 +# Author: Markus Wenzel, TU Muenchen
     9.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     9.9  #
    9.10  # DESCRIPTION: replace goal(w) commands by implicit versions Goal(w)
    9.11  
    9.12  
    9.13  ## diagnostics
    9.14  
    9.15 -PRG=$(basename $0)
    9.16 +PRG=$(basename "$0")
    9.17  
    9.18  function usage()
    9.19  {
    9.20 @@ -25,9 +27,9 @@
    9.21  
    9.22  ## process command line
    9.23  
    9.24 -[ $# -eq 0 -o "$1" = "-?" ] && usage
    9.25 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    9.26  
    9.27 -SPECS="$@"; shift $#
    9.28 +SPECS="$@"; shift "$#"
    9.29  
    9.30  
    9.31  ## main
    9.32 @@ -35,4 +37,4 @@
    9.33  #set by configure
    9.34  AUTO_PERL=perl
    9.35  
    9.36 -find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixgoal.pl
    9.37 +find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgoal.pl"
    10.1 --- a/lib/Tools/fixseq	Fri Sep 01 17:48:31 2000 +0200
    10.2 +++ b/lib/Tools/fixseq	Fri Sep 01 17:50:36 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  # DESCRIPTION: fix references to obsolete Pure/Sequence structure
   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 @@ -25,9 +27,9 @@
   10.21  
   10.22  ## process command line
   10.23  
   10.24 -[ $# -eq 0 -o "$1" = "-?" ] && usage
   10.25 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
   10.26  
   10.27 -SPECS="$@"; shift $#
   10.28 +SPECS="$@"; shift "$#"
   10.29  
   10.30  
   10.31  ## main
   10.32 @@ -35,4 +37,4 @@
   10.33  #set by configure
   10.34  AUTO_PERL=perl
   10.35  
   10.36 -find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixseq.pl
   10.37 +find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixseq.pl"
    11.1 --- a/lib/Tools/getenv	Fri Sep 01 17:48:31 2000 +0200
    11.2 +++ b/lib/Tools/getenv	Fri Sep 01 17:50:36 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  # DESCRIPTION: get values from Isabelle settings environment
   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 @@ -51,7 +53,7 @@
   11.21  
   11.22  # args
   11.23  
   11.24 -[ -n "$ALL" -a $# -ne 0 ] && usage
   11.25 +[ -n "$ALL" -a "$#" -ne 0 ] && usage
   11.26  
   11.27  
   11.28  ## main
   11.29 @@ -59,7 +61,7 @@
   11.30  if [ -n "$ALL" ]; then
   11.31    env | sort
   11.32  else
   11.33 -  for VAR in $*
   11.34 +  for VAR in "$@"
   11.35    do
   11.36      if [ -n "$BASE" ]; then
   11.37        eval "echo \$$VAR"
    12.1 --- a/lib/Tools/install	Fri Sep 01 17:48:31 2000 +0200
    12.2 +++ b/lib/Tools/install	Fri Sep 01 17:50:36 2000 +0200
    12.3 @@ -1,11 +1,13 @@
    12.4  #!/bin/bash
    12.5  #
    12.6  # $Id$
    12.7 +# Author: Markus Wenzel, TU Muenchen
    12.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    12.9  #
   12.10  # DESCRIPTION: install standalone Isabelle executables
   12.11  
   12.12  
   12.13 -PRG=$(basename $0)
   12.14 +PRG=$(basename "$0")
   12.15  
   12.16  function usage()
   12.17  {
   12.18 @@ -67,7 +69,7 @@
   12.19  
   12.20  # args
   12.21  
   12.22 -[ $# -ne 0 -o -n "$NO_OPTS" ] && usage
   12.23 +[ "$#" -ne 0 -o -n "$NO_OPTS" ] && usage
   12.24  
   12.25  
   12.26  ## main
   12.27 @@ -88,10 +90,10 @@
   12.28      BIN="$BINDIR/$NAME"
   12.29      DIST="$DISTDIR/bin/$NAME"
   12.30      echo "installing $BIN"
   12.31 -    echo "#!$AUTO_BASH" >$BIN || fail "Cannot write file: $BIN"
   12.32 -    echo >>$BIN
   12.33 -    echo "exec $DIST \"\$@\"" >>$BIN
   12.34 -    chmod +x $BIN
   12.35 +    echo "#!$AUTO_BASH" > "$BIN" || fail "Cannot write file: $BIN"
   12.36 +    echo >> "$BIN"
   12.37 +    echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
   12.38 +    chmod +x "$BIN"
   12.39    done
   12.40  fi
   12.41  
   12.42 @@ -100,28 +102,28 @@
   12.43  
   12.44  KDEHOME=~/.kde
   12.45  KDEAPP=~/Desktop/Isabelle.kdelnk
   12.46 -KDEICONS=$KDEHOME/share/icons
   12.47 +KDEICONS="$KDEHOME/share/icons"
   12.48  
   12.49  if [ "$KDE" = true ]; then
   12.50 -  mkdir -p $KDEICONS || fail "Bad directory: $KDEICONS"
   12.51 -  mkdir -p $KDEICONS/mini || fail "Bad directory: $KDEICONS/mini"
   12.52 +  mkdir -p "$KDEICONS" || fail "Bad directory: $KDEICONS"
   12.53 +  mkdir -p "$KDEICONS/mini" || fail "Bad directory: $KDEICONS/mini"
   12.54  
   12.55 -  [ -f $KDEICONS/isabelle.xpm ] || cp $ISABELLE_HOME/lib/icons/isabelle.xpm $KDEICONS || \
   12.56 +  [ -f "$KDEICONS/isabelle.xpm" ] || cp "$ISABELLE_HOME/lib/icons/isabelle.xpm" "$KDEICONS" || \
   12.57      fail "Cannot write file: $KDEICONS/isabelle.xpm"
   12.58 -  [ -f $KDEICONS/mini/isabelle.xpm ] || \
   12.59 -    cp $ISABELLE_HOME/lib/icons/isabelle-mini.xpm $KDEICONS/mini/isabelle.xpm || \
   12.60 +  [ -f "$KDEICONS/mini/isabelle.xpm" ] || \
   12.61 +    cp "$ISABELLE_HOME/lib/icons/isabelle-mini.xpm" "$KDEICONS/mini/isabelle.xpm" || \
   12.62      fail "Cannot write file: $KDEICONS/mini/isabelle.xpm"
   12.63  
   12.64    echo "installing $KDEAPP"
   12.65 -  echo "# KDE Config File" >$KDEAPP || fail "Cannot write file: $KDEAPP"
   12.66 -  echo "[KDE Desktop Entry]" >>$KDEAPP
   12.67 -  echo "Type=Application" >>$KDEAPP
   12.68 -  echo "Exec=$DISTDIR/bin/Isabelle %f" >>$KDEAPP
   12.69 -  echo "Icon=isabelle.xpm" >>$KDEAPP
   12.70 -  echo "TerminalOptions=" >>$KDEAPP
   12.71 -  echo "Path=" >>$KDEAPP
   12.72 -  echo "Terminal=0" >>$KDEAPP
   12.73 -  echo "Name=Isabelle" >>$KDEAPP
   12.74 +  echo "# KDE Config File" > "$KDEAPP" || fail "Cannot write file: $KDEAPP"
   12.75 +  echo "[KDE Desktop Entry]" >> "$KDEAPP"
   12.76 +  echo "Type=Application" >> "$KDEAPP"
   12.77 +  echo "Exec=$DISTDIR/bin/Isabelle %f" >> "$KDEAPP"
   12.78 +  echo "Icon=isabelle.xpm" >> "$KDEAPP"
   12.79 +  echo "TerminalOptions=" >> "$KDEAPP"
   12.80 +  echo "Path=" >> "$KDEAPP"
   12.81 +  echo "Terminal=0" >> "$KDEAPP"
   12.82 +  echo "Name=Isabelle" >> "$KDEAPP"
   12.83  
   12.84 -  type -p kfmclient >/dev/null && kfmclient refreshDesktop
   12.85 +  echo "Please refresh your KDE now!"
   12.86  fi
    13.1 --- a/lib/Tools/installfonts	Fri Sep 01 17:48:31 2000 +0200
    13.2 +++ b/lib/Tools/installfonts	Fri Sep 01 17:50:36 2000 +0200
    13.3 @@ -1,11 +1,13 @@
    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  # DESCRIPTION: install the isabelle fonts into your X11 server
   13.11  
   13.12  
   13.13 -PRG=$(basename $0)
   13.14 +PRG=$(basename "$0")
   13.15  
   13.16  function usage()
   13.17  {
   13.18 @@ -37,7 +39,7 @@
   13.19  
   13.20  ## main
   13.21  
   13.22 -[ $# -ne 0 ] && usage
   13.23 +[ "$#" -ne 0 ] && usage
   13.24  
   13.25  checkfonts || eval $ISABELLE_INSTALLFONTS
   13.26  checkfonts || echo "WARNING: Isabelle fonts probably not installed correctly!" >&2
    14.1 --- a/lib/Tools/latex	Fri Sep 01 17:48:31 2000 +0200
    14.2 +++ b/lib/Tools/latex	Fri Sep 01 17:50:36 2000 +0200
    14.3 @@ -1,11 +1,13 @@
    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  # DESCRIPTION: run LaTeX (and related tools)
   14.11  
   14.12  
   14.13 -PRG=$(basename $0)
   14.14 +PRG=$(basename "$0")
   14.15  
   14.16  function usage()
   14.17  {
   14.18 @@ -53,9 +55,9 @@
   14.19  # args
   14.20  
   14.21  FILE="root.tex"
   14.22 -[ $# -ge 1 ] && { FILE="$1"; shift; }
   14.23 +[ "$#" -ge 1 ] && { FILE="$1"; shift; }
   14.24  
   14.25 -[ $# -ne 0 ] && usage
   14.26 +[ "$#" -ne 0 ] && usage
   14.27  
   14.28  
   14.29  ## main
   14.30 @@ -63,11 +65,8 @@
   14.31  # root file
   14.32  
   14.33  DIR=$(dirname "$FILE")
   14.34 -if [ "$DIR" = . ]; then
   14.35 -  FILEBASE=$(basename "$FILE" .tex)
   14.36 -else
   14.37 -  FILEBASE=$DIR/$(basename "$FILE" .tex)
   14.38 -fi
   14.39 +FILEBASE=$(basename "$FILE" .tex)
   14.40 +[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
   14.41  
   14.42  function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
   14.43  
   14.44 @@ -82,7 +81,7 @@
   14.45  
   14.46  function update_styles ()
   14.47  {
   14.48 -  for NAME in $ISABELLE_HOME/lib/texinputs/*.sty
   14.49 +  for NAME in "$ISABELLE_HOME/lib/texinputs"/*.sty
   14.50    do
   14.51      DEST="$DIR"/$(basename "$NAME")
   14.52      if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then
   14.53 @@ -96,49 +95,49 @@
   14.54    dvi)
   14.55      check_root && \
   14.56      run_latex
   14.57 -    RC=$?
   14.58 +    RC="$?"
   14.59      ;;
   14.60    dvi.gz)
   14.61      check_root && \
   14.62      run_latex && \
   14.63      gzip -f "$FILEBASE.dvi"
   14.64 -    RC=$?
   14.65 +    RC="$?"
   14.66      ;;
   14.67    ps)
   14.68      check_root && \
   14.69      run_latex && \
   14.70      run_dvips &&
   14.71 -    RC=$?
   14.72 +    RC="$?"
   14.73      ;;
   14.74    ps.gz)
   14.75      check_root && \
   14.76      run_latex && \
   14.77      run_dvips &&
   14.78      gzip -f "$FILEBASE.ps"
   14.79 -    RC=$?
   14.80 +    RC="$?"
   14.81      ;;
   14.82    pdf)
   14.83      check_root && \
   14.84      run_pdflatex
   14.85 -    RC=$?
   14.86 +    RC="$?"
   14.87      ;;
   14.88    bbl)
   14.89      check_root && \
   14.90      run_bibtex
   14.91 -    RC=$?
   14.92 +    RC="$?"
   14.93      ;;
   14.94    png)
   14.95      check_root && \
   14.96      run_thumbpdf
   14.97 -    RC=$?
   14.98 +    RC="$?"
   14.99      ;;
  14.100    sty)
  14.101      update_styles
  14.102 -    RC=$?
  14.103 +    RC="$?"
  14.104      ;;
  14.105    *)
  14.106      fail "Bad output format '$OUTFORMAT'"
  14.107      ;;
  14.108  esac
  14.109  
  14.110 -exit $RC
  14.111 +exit "$RC"
    15.1 --- a/lib/Tools/logo	Fri Sep 01 17:48:31 2000 +0200
    15.2 +++ b/lib/Tools/logo	Fri Sep 01 17:50:36 2000 +0200
    15.3 @@ -1,11 +1,13 @@
    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  # DESCRIPTION: create an instance of the Isabelle logo
   15.11  
   15.12  
   15.13 -PRG=$(basename $0)
   15.14 +PRG=$(basename "$0")
   15.15  
   15.16  function usage()
   15.17  {
   15.18 @@ -56,9 +58,9 @@
   15.19  # args
   15.20  
   15.21  NAME="-"
   15.22 -[ $# -ge 1 ] && { NAME="$1"; shift; }
   15.23 +[ "$#" -ge 1 ] && { NAME="$1"; shift; }
   15.24  
   15.25 -[ $# -ne 0 -o "$NAME" = "-" ] && usage
   15.26 +[ "$#" -ne 0 -o "$NAME" = "-" ] && usage
   15.27  
   15.28  
   15.29  ## main
   15.30 @@ -73,8 +75,8 @@
   15.31  AUTO_PERL=perl
   15.32  
   15.33  if [ "$OUTFILE" = "-" ]; then
   15.34 -  $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
   15.35 +  "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps"
   15.36  else
   15.37    [ -z "$QUIET" ] && echo "$OUTFILE" >&2
   15.38 -  $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
   15.39 +  "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE"
   15.40  fi
    16.1 --- a/lib/Tools/make	Fri Sep 01 17:48:31 2000 +0200
    16.2 +++ b/lib/Tools/make	Fri Sep 01 17:50:36 2000 +0200
    16.3 @@ -1,11 +1,13 @@
    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  # DESCRIPTION: Isabelle make utility
   16.11  
   16.12  
   16.13 -PRG=$(basename $0)
   16.14 +PRG=$(basename "$0")
   16.15  
   16.16  function usage()
   16.17  {
    17.1 --- a/lib/Tools/makeall	Fri Sep 01 17:48:31 2000 +0200
    17.2 +++ b/lib/Tools/makeall	Fri Sep 01 17:50:36 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  # DESCRIPTION: apply make utility to all logics
   17.11  
   17.12 @@ -11,7 +13,7 @@
   17.13  
   17.14  ## diagnostics
   17.15  
   17.16 -PRG=$(basename $0)
   17.17 +PRG=$(basename "$0")
   17.18  
   17.19  function usage()
   17.20  {
   17.21 @@ -36,10 +38,10 @@
   17.22  
   17.23  for L in $ALL_LOGICS
   17.24  do
   17.25 -  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make "$@" )
   17.26 +  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" )
   17.27  done
   17.28  
   17.29  echo -n "Finished at "; date
   17.30  
   17.31 -ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
   17.32 +ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
   17.33  echo "$ELAPSED total elapsed time"
    18.1 --- a/lib/Tools/mkdir	Fri Sep 01 17:48:31 2000 +0200
    18.2 +++ b/lib/Tools/mkdir	Fri Sep 01 17:50:36 2000 +0200
    18.3 @@ -1,13 +1,15 @@
    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  # DESCRIPTION: prepare logic session directory
   18.11  
   18.12  
   18.13  ## diagnostics
   18.14  
   18.15 -PRG=$(basename $0)
   18.16 +PRG=$(basename "$0")
   18.17  
   18.18  function usage()
   18.19  {
   18.20 @@ -69,10 +71,10 @@
   18.21  # args
   18.22  
   18.23  
   18.24 -if [ $# -eq 1 ]; then
   18.25 +if [ "$#" -eq 1 ]; then
   18.26    LOGIC="$ISABELLE_LOGIC"
   18.27    DIR_NAME="$1"; shift
   18.28 -elif [ $# -eq 2 ]; then
   18.29 +elif [ "$#" -eq 2 ]; then
   18.30    LOGIC="$1"; shift
   18.31    DIR_NAME="$1"; shift
   18.32  else
    19.1 --- a/lib/Tools/nonascii	Fri Sep 01 17:48:31 2000 +0200
    19.2 +++ b/lib/Tools/nonascii	Fri Sep 01 17:50:36 2000 +0200
    19.3 @@ -1,13 +1,15 @@
    19.4  #!/bin/bash
    19.5  #
    19.6  # $Id$
    19.7 +# Author: Markus Wenzel, TU Muenchen
    19.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    19.9  #
   19.10  # DESCRIPTION: check files for non-ASCII characters
   19.11  
   19.12  
   19.13  ## diagnostics
   19.14  
   19.15 -PRG=$(basename $0)
   19.16 +PRG=$(basename "$0")
   19.17  
   19.18  function usage()
   19.19  {
   19.20 @@ -22,9 +24,9 @@
   19.21  
   19.22  ## process command line
   19.23  
   19.24 -[ $# -eq 0 -o "$1" = "-?" ] && usage
   19.25 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
   19.26  
   19.27 -SPECS="$@"; shift $#
   19.28 +SPECS="$@"; shift "$#"
   19.29  
   19.30  
   19.31  ## main
   19.32 @@ -33,5 +35,5 @@
   19.33  AUTO_PERL=perl
   19.34  
   19.35  find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
   19.36 -  xargs $AUTO_PERL -w -e \
   19.37 +  xargs "$AUTO_PERL" -w -e \
   19.38      'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'
    20.1 --- a/lib/Tools/symbolinput	Fri Sep 01 17:48:31 2000 +0200
    20.2 +++ b/lib/Tools/symbolinput	Fri Sep 01 17:50:36 2000 +0200
    20.3 @@ -1,10 +1,12 @@
    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  # DESCRIPTION: translate symbols into \<...> sequences
   20.11  
   20.12  #set by configure
   20.13  AUTO_PERL=perl
   20.14  
   20.15 -exec $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
   20.16 +exec "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/symbolinput.pl" "$@"
    21.1 --- a/lib/Tools/usedir	Fri Sep 01 17:48:31 2000 +0200
    21.2 +++ b/lib/Tools/usedir	Fri Sep 01 17:50:36 2000 +0200
    21.3 @@ -1,13 +1,15 @@
    21.4  #!/bin/bash
    21.5  #
    21.6  # $Id$
    21.7 +# Author: Markus Wenzel, TU Muenchen
    21.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
    21.9  #
   21.10  # DESCRIPTION: build object-logic or run examples
   21.11  
   21.12  
   21.13  ## diagnostics
   21.14  
   21.15 -PRG=$(basename $0)
   21.16 +PRG=$(basename "$0")
   21.17  
   21.18  function usage()
   21.19  {
   21.20 @@ -92,12 +94,12 @@
   21.21  
   21.22  # args
   21.23  
   21.24 -[ $# -ne 2 ] && usage
   21.25 +[ "$#" -ne 2 ] && usage
   21.26  
   21.27  LOGIC="$1"; shift
   21.28  NAME="$1"; shift
   21.29  
   21.30 -[ -z "$SESSION" ] && SESSION=$(basename $NAME)
   21.31 +[ -z "$SESSION" ] && SESSION=$(basename "$NAME")
   21.32  
   21.33  
   21.34  
   21.35 @@ -105,10 +107,10 @@
   21.36  
   21.37  # prepare browser info dir
   21.38  
   21.39 -if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then
   21.40 -  mkdir -p $ISABELLE_BROWSER_INFO
   21.41 -  cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/isabelle.gif
   21.42 -  cp $ISABELLE_HOME/lib/html/index.html $ISABELLE_BROWSER_INFO/index.html
   21.43 +if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
   21.44 +  mkdir -p "$ISABELLE_BROWSER_INFO"
   21.45 +  cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
   21.46 +  cp "$ISABELLE_HOME/lib/html/index.html" "$ISABELLE_BROWSER_INFO/index.html"
   21.47  fi
   21.48  
   21.49  
   21.50 @@ -126,7 +128,7 @@
   21.51  
   21.52  if [ "$DOCUMENT" != false -a -d document ]; then
   21.53    DOC="$DOCUMENT"
   21.54 -  [ -n "$DUMP" -a -d "$DUMP" ] && $ISATOOL latex -o sty "$DUMP/root.tex" >/dev/null
   21.55 +  [ -n "$DUMP" -a -d "$DUMP" ] && "$ISATOOL" latex -o sty "$DUMP/root.tex" >/dev/null
   21.56  else
   21.57    DOC=""
   21.58  fi
   21.59 @@ -142,34 +144,34 @@
   21.60    OPT_C=""
   21.61    [ "$COMPRESS" = true ] && OPT_C="-c"
   21.62  
   21.63 -  $ISABELLE \
   21.64 +  "$ISABELLE" \
   21.65      -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \
   21.66 -    $OPT_C -q -w $LOGIC $NAME > $LOG 2>&1
   21.67 -  RC=$?
   21.68 +    $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1
   21.69 +  RC="$?"
   21.70  else
   21.71 -  ITEM=$(basename $LOGIC)-"$SESSION"
   21.72 +  ITEM=$(basename "$LOGIC")-"$SESSION"
   21.73    echo "Running $ITEM ..."
   21.74    LOG="$LOGDIR/$ITEM"
   21.75  
   21.76 -  $ISABELLE \
   21.77 +  "$ISABELLE" \
   21.78      -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\"; quit();" \
   21.79 -    -r -q $LOGIC > $LOG 2>&1
   21.80 -  RC=$?
   21.81 +    -r -q "$LOGIC" > "$LOG" 2>&1
   21.82 +  RC="$?"
   21.83    cd ..
   21.84  fi
   21.85  
   21.86 -ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
   21.87 +ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
   21.88  
   21.89  
   21.90  # exit status
   21.91  
   21.92 -if [ $RC -eq 0 ]; then
   21.93 +if [ "$RC" -eq 0 ]; then
   21.94    echo "Finished $ITEM ($ELAPSED elapsed time)"
   21.95    gzip --force "$LOG"
   21.96  else
   21.97    echo "$ITEM FAILED"
   21.98    echo "(see also $LOG)"
   21.99 -  echo; tail $LOG; echo
  21.100 +  echo; tail "$LOG"; echo
  21.101  fi
  21.102  
  21.103 -exit $RC
  21.104 +exit "$RC"