Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
GPLed;
authorwenzelm
Fri, 01 Sep 2000 17:50:36 +0200
changeset 9788 df671fa2562a
parent 9787 fb8c5a66dbe8
child 9789 7e5e6c47c0b5
GPLed; more robust handling of spaces in args / file names;
lib/Tools/browser file | annotate | diff | comparison | revisions
lib/Tools/doc file | annotate | diff | comparison | revisions
lib/Tools/document file | annotate | diff | comparison | revisions
lib/Tools/expandshort file | annotate | diff | comparison | revisions
lib/Tools/findlogics file | annotate | diff | comparison | revisions
lib/Tools/fixclasimp file | annotate | diff | comparison | revisions
lib/Tools/fixdatatype file | annotate | diff | comparison | revisions
lib/Tools/fixdots file | annotate | diff | comparison | revisions
lib/Tools/fixgoal file | annotate | diff | comparison | revisions
lib/Tools/fixseq file | annotate | diff | comparison | revisions
lib/Tools/getenv file | annotate | diff | comparison | revisions
lib/Tools/install file | annotate | diff | comparison | revisions
lib/Tools/installfonts file | annotate | diff | comparison | revisions
lib/Tools/latex file | annotate | diff | comparison | revisions
lib/Tools/logo file | annotate | diff | comparison | revisions
lib/Tools/make file | annotate | diff | comparison | revisions
lib/Tools/makeall file | annotate | diff | comparison | revisions
lib/Tools/mkdir file | annotate | diff | comparison | revisions
lib/Tools/nonascii file | annotate | diff | comparison | revisions
lib/Tools/symbolinput file | annotate | diff | comparison | revisions
lib/Tools/usedir file | annotate | diff | comparison | revisions 
--- a/lib/Tools/browser	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/browser	Fri Sep 01 17:50:36 2000 +0200
@@ -1,11 +1,13 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: Isabelle graph browser
 
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -42,14 +44,14 @@
 # args
 
 GRAPHFILE=""
-[ $# -gt 0 ] && { GRAPHFILE="$1"; shift; }
-[ $# -ne 0 ] && usage
+[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
+[ "$#" -ne 0 ] && usage
 
 
 ## main
 
-export CLASSPATH=$ISABELLE_HOME/lib/browser
-[ -z "$GRAPHFILE" ] && cd $ISABELLE_BROWSER_INFO
+export CLASSPATH="$ISABELLE_HOME/lib/browser"
+[ -z "$GRAPHFILE" ] && cd "$ISABELLE_BROWSER_INFO"
 
-java GraphBrowser.GraphBrowser $GRAPHFILE
+java GraphBrowser.GraphBrowser "$GRAPHFILE"
 [ -n "$GRAPHFILE" -a -n "$DELETE" ] && rm -f "$GRAPHFILE"
--- a/lib/Tools/doc	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/doc	Fri Sep 01 17:50:36 2000 +0200
@@ -1,11 +1,13 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: view Isabelle documentation
 
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -27,24 +29,28 @@
 ## args
 
 DOC=""
-[ $# -ge 1 ] && { DOC="$1"; shift; }
+[ "$#" -ge 1 ] && { DOC="$1"; shift; }
 
-[ $# -ne 0 -o "$DOC" = "-?" ] && usage
+[ "$#" -ne 0 -o "$DOC" = "-?" ] && usage
 
 
 ## main
 
-DOCS=$(echo $ISABELLE_DOCS | tr : " ")
-
 if [ -z "$DOC" ]; then
-  for DIR in $DOCS
+  ORIG_IFS="$IFS"
+  IFS=":"
+  for DIR in $ISABELLE_DOCS
   do
-    [ -f $DIR/Contents ] && grep -v "^>>" $DIR/Contents
+    [ -f "$DIR/Contents" ] && grep -v "^>>" "$DIR/Contents"
   done
+  IFS="$ORIG_IFS"
 else
-  for DIR in $DOCS
+  ORIG_IFS="$IFS"
+  IFS=":"
+  for DIR in $ISABELLE_DOCS
   do
-    [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
+    [ -f "$DIR/$DOC.dvi" ] && { cd "$DIR"; IFS="$ORIG_IFS"; exec $DVI_VIEWER "$DOC.dvi"; }
   done
+  IFS="$ORIG_IFS"
   fail "Unknown Isabelle document: $DOC"  
 fi
--- a/lib/Tools/document	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/document	Fri Sep 01 17:50:36 2000 +0200
@@ -1,11 +1,13 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: prepare theory session document
 
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -58,9 +60,9 @@
 # args
 
 DIR="document"
-[ $# -ge 1 ] && { DIR="$1"; shift; }
+[ "$#" -ge 1 ] && { DIR="$1"; shift; }
 
-[ $# -ne 0 ] && usage
+[ "$#" -ne 0 ] && usage
 
 
 ## main
@@ -84,11 +86,11 @@
   [ -n "$CLEAN" ] && rm -f *.aux *.out
   if [ -f root.bib ]
   then
-    $ISATOOL latex -o "$FMT" && \
-    $ISATOOL latex -o bbl && \
-    $ISATOOL latex -o "$FMT"
+    "$ISATOOL" latex -o "$FMT" && \
+    "$ISATOOL" latex -o bbl && \
+    "$ISATOOL" latex -o "$FMT"
   else
-    $ISATOOL latex -o "$FMT"
+    "$ISATOOL" latex -o "$FMT"
   fi
 }
 
@@ -98,20 +100,20 @@
   [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT"
 
   if [ -f IsaMakefile ]; then
-    $ISATOOL make "$OUTFORMAT"
-    RC=$?
+    "$ISATOOL" make "$OUTFORMAT"
+    RC="$?"
   elif [ "$OUTFORMAT" = pdf ]; then
     pre_latex pdf && \
-    $ISATOOL latex -o pdf && \
+    "$ISATOOL" latex -o pdf && \
     { if [ -n "$ISABELLE_THUMBPDF" ]; then
-        $ISATOOL latex -o png && \
-        $ISATOOL latex -o pdf
+        "$ISATOOL" latex -o png && \
+        "$ISATOOL" latex -o pdf
       fi; }
-    RC=$?
+    RC="$?"
   else
     pre_latex dvi && \
-    $ISATOOL latex -o "$OUTFORMAT"
-    RC=$?
+    "$ISATOOL" latex -o "$OUTFORMAT"
+    RC="$?"
   fi
 
   [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
@@ -119,7 +121,7 @@
 
   exit "$RC"
 )
-RC=$?
+RC="$?"
 
 
 # install
--- a/lib/Tools/expandshort	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/expandshort	Fri Sep 01 17:50:36 2000 +0200
@@ -1,11 +1,13 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: expand shorthand goal commands
 
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -25,9 +27,9 @@
 
 ## process command line
 
-[ $# -eq 0 -o "$1" = "-?" ] && usage
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
 
-SPECS="$@"; shift $#
+SPECS="$@"; shift "$#"
 
 
 ## main
@@ -35,4 +37,4 @@
 #set by configure
 AUTO_PERL=perl
 
-find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/expandshort.pl
+find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/expandshort.pl"
--- a/lib/Tools/findlogics	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/findlogics	Fri Sep 01 17:50:36 2000 +0200
@@ -1,11 +1,13 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: collect heap names from ISABELLE_PATH
 
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -20,14 +22,17 @@
 
 ## main
 
-[ $# -ne 0 ] && usage
+[ "$#" -ne 0 ] && usage
 
 
 LOGICS=""
 
-for DIR in $(echo $ISABELLE_PATH | tr : " ")
+ORIG_IFS="$IFS"
+IFS=":"
+for DIR in $ISABELLE_PATH
 do
-  for FILE in $DIR/*
+  DIR="$DIR/$ML_IDENTIFIER"
+  for FILE in "$DIR"/*
   do
     if [ -f "$FILE" ]; then
       NAME=$(basename "$FILE")
@@ -35,5 +40,6 @@
     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)
--- a/lib/Tools/fixclasimp	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/fixclasimp	Fri Sep 01 17:50:36 2000 +0200
@@ -1,13 +1,15 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: fix references to implicit claset and simpset
 
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -25,9 +27,9 @@
 
 ## process command line
 
-[ $# -eq 0 -o "$1" = "-?" ] && usage
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
 
-SPECS="$@"; shift $#
+SPECS="$@"; shift "$#"
 
 
 ## main
@@ -35,4 +37,4 @@
 #set by configure
 AUTO_PERL=perl
 
-find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixclasimp.pl
+find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixclasimp.pl"
--- a/lib/Tools/fixdatatype	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/fixdatatype	Fri Sep 01 17:50:36 2000 +0200
@@ -1,13 +1,15 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: adapt theories and proof scripts to new datatype package
 
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -25,9 +27,9 @@
 
 ## process command line
 
-[ $# -eq 0 -o "$1" = "-?" ] && usage
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
 
-SPECS="$@"; shift $#
+SPECS="$@"; shift "$#"
 
 
 ## main
@@ -36,4 +38,4 @@
 AUTO_PERL=perl
 
 find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
-  xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixdatatype.pl
+  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixdatatype.pl"
--- a/lib/Tools/fixdots	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/fixdots	Fri Sep 01 17:50:36 2000 +0200
@@ -1,13 +1,15 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: ensure that dots in formulas are followed by non-idents
 
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -25,9 +27,9 @@
 
 ## process command line
 
-[ $# -eq 0 -o "$1" = "-?" ] && usage
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
 
-SPECS="$@"; shift $#
+SPECS="$@"; shift "$#"
 
 
 ## main
@@ -36,4 +38,4 @@
 AUTO_PERL=perl
 
 find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
-  xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixdots.pl
+  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixdots.pl"
--- a/lib/Tools/fixgoal	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/fixgoal	Fri Sep 01 17:50:36 2000 +0200
@@ -1,13 +1,15 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: replace goal(w) commands by implicit versions Goal(w)
 
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -25,9 +27,9 @@
 
 ## process command line
 
-[ $# -eq 0 -o "$1" = "-?" ] && usage
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
 
-SPECS="$@"; shift $#
+SPECS="$@"; shift "$#"
 
 
 ## main
@@ -35,4 +37,4 @@
 #set by configure
 AUTO_PERL=perl
 
-find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixgoal.pl
+find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgoal.pl"
--- a/lib/Tools/fixseq	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/fixseq	Fri Sep 01 17:50:36 2000 +0200
@@ -1,13 +1,15 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: fix references to obsolete Pure/Sequence structure
 
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -25,9 +27,9 @@
 
 ## process command line
 
-[ $# -eq 0 -o "$1" = "-?" ] && usage
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
 
-SPECS="$@"; shift $#
+SPECS="$@"; shift "$#"
 
 
 ## main
@@ -35,4 +37,4 @@
 #set by configure
 AUTO_PERL=perl
 
-find $SPECS -name \*.ML -print | xargs $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/fixseq.pl
+find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixseq.pl"
--- a/lib/Tools/getenv	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/getenv	Fri Sep 01 17:50:36 2000 +0200
@@ -1,13 +1,15 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: get values from Isabelle settings environment
 
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -51,7 +53,7 @@
 
 # args
 
-[ -n "$ALL" -a $# -ne 0 ] && usage
+[ -n "$ALL" -a "$#" -ne 0 ] && usage
 
 
 ## main
@@ -59,7 +61,7 @@
 if [ -n "$ALL" ]; then
   env | sort
 else
-  for VAR in $*
+  for VAR in "$@"
   do
     if [ -n "$BASE" ]; then
       eval "echo \$$VAR"
--- a/lib/Tools/install	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/install	Fri Sep 01 17:50:36 2000 +0200
@@ -1,11 +1,13 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: install standalone Isabelle executables
 
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -67,7 +69,7 @@
 
 # args
 
-[ $# -ne 0 -o -n "$NO_OPTS" ] && usage
+[ "$#" -ne 0 -o -n "$NO_OPTS" ] && usage
 
 
 ## main
@@ -88,10 +90,10 @@
     BIN="$BINDIR/$NAME"
     DIST="$DISTDIR/bin/$NAME"
     echo "installing $BIN"
-    echo "#!$AUTO_BASH" >$BIN || fail "Cannot write file: $BIN"
-    echo >>$BIN
-    echo "exec $DIST \"\$@\"" >>$BIN
-    chmod +x $BIN
+    echo "#!$AUTO_BASH" > "$BIN" || fail "Cannot write file: $BIN"
+    echo >> "$BIN"
+    echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
+    chmod +x "$BIN"
   done
 fi
 
@@ -100,28 +102,28 @@
 
 KDEHOME=~/.kde
 KDEAPP=~/Desktop/Isabelle.kdelnk
-KDEICONS=$KDEHOME/share/icons
+KDEICONS="$KDEHOME/share/icons"
 
 if [ "$KDE" = true ]; then
-  mkdir -p $KDEICONS || fail "Bad directory: $KDEICONS"
-  mkdir -p $KDEICONS/mini || fail "Bad directory: $KDEICONS/mini"
+  mkdir -p "$KDEICONS" || fail "Bad directory: $KDEICONS"
+  mkdir -p "$KDEICONS/mini" || fail "Bad directory: $KDEICONS/mini"
 
-  [ -f $KDEICONS/isabelle.xpm ] || cp $ISABELLE_HOME/lib/icons/isabelle.xpm $KDEICONS || \
+  [ -f "$KDEICONS/isabelle.xpm" ] || cp "$ISABELLE_HOME/lib/icons/isabelle.xpm" "$KDEICONS" || \
     fail "Cannot write file: $KDEICONS/isabelle.xpm"
-  [ -f $KDEICONS/mini/isabelle.xpm ] || \
-    cp $ISABELLE_HOME/lib/icons/isabelle-mini.xpm $KDEICONS/mini/isabelle.xpm || \
+  [ -f "$KDEICONS/mini/isabelle.xpm" ] || \
+    cp "$ISABELLE_HOME/lib/icons/isabelle-mini.xpm" "$KDEICONS/mini/isabelle.xpm" || \
     fail "Cannot write file: $KDEICONS/mini/isabelle.xpm"
 
   echo "installing $KDEAPP"
-  echo "# KDE Config File" >$KDEAPP || fail "Cannot write file: $KDEAPP"
-  echo "[KDE Desktop Entry]" >>$KDEAPP
-  echo "Type=Application" >>$KDEAPP
-  echo "Exec=$DISTDIR/bin/Isabelle %f" >>$KDEAPP
-  echo "Icon=isabelle.xpm" >>$KDEAPP
-  echo "TerminalOptions=" >>$KDEAPP
-  echo "Path=" >>$KDEAPP
-  echo "Terminal=0" >>$KDEAPP
-  echo "Name=Isabelle" >>$KDEAPP
+  echo "# KDE Config File" > "$KDEAPP" || fail "Cannot write file: $KDEAPP"
+  echo "[KDE Desktop Entry]" >> "$KDEAPP"
+  echo "Type=Application" >> "$KDEAPP"
+  echo "Exec=$DISTDIR/bin/Isabelle %f" >> "$KDEAPP"
+  echo "Icon=isabelle.xpm" >> "$KDEAPP"
+  echo "TerminalOptions=" >> "$KDEAPP"
+  echo "Path=" >> "$KDEAPP"
+  echo "Terminal=0" >> "$KDEAPP"
+  echo "Name=Isabelle" >> "$KDEAPP"
 
-  type -p kfmclient >/dev/null && kfmclient refreshDesktop
+  echo "Please refresh your KDE now!"
 fi
--- a/lib/Tools/installfonts	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/installfonts	Fri Sep 01 17:50:36 2000 +0200
@@ -1,11 +1,13 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: install the isabelle fonts into your X11 server
 
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -37,7 +39,7 @@
 
 ## main
 
-[ $# -ne 0 ] && usage
+[ "$#" -ne 0 ] && usage
 
 checkfonts || eval $ISABELLE_INSTALLFONTS
 checkfonts || echo "WARNING: Isabelle fonts probably not installed correctly!" >&2
--- a/lib/Tools/latex	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/latex	Fri Sep 01 17:50:36 2000 +0200
@@ -1,11 +1,13 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: run LaTeX (and related tools)
 
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -53,9 +55,9 @@
 # args
 
 FILE="root.tex"
-[ $# -ge 1 ] && { FILE="$1"; shift; }
+[ "$#" -ge 1 ] && { FILE="$1"; shift; }
 
-[ $# -ne 0 ] && usage
+[ "$#" -ne 0 ] && usage
 
 
 ## main
@@ -63,11 +65,8 @@
 # root file
 
 DIR=$(dirname "$FILE")
-if [ "$DIR" = . ]; then
-  FILEBASE=$(basename "$FILE" .tex)
-else
-  FILEBASE=$DIR/$(basename "$FILE" .tex)
-fi
+FILEBASE=$(basename "$FILE" .tex)
+[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
 
 function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
 
@@ -82,7 +81,7 @@
 
 function update_styles ()
 {
-  for NAME in $ISABELLE_HOME/lib/texinputs/*.sty
+  for NAME in "$ISABELLE_HOME/lib/texinputs"/*.sty
   do
     DEST="$DIR"/$(basename "$NAME")
     if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then
@@ -96,49 +95,49 @@
   dvi)
     check_root && \
     run_latex
-    RC=$?
+    RC="$?"
     ;;
   dvi.gz)
     check_root && \
     run_latex && \
     gzip -f "$FILEBASE.dvi"
-    RC=$?
+    RC="$?"
     ;;
   ps)
     check_root && \
     run_latex && \
     run_dvips &&
-    RC=$?
+    RC="$?"
     ;;
   ps.gz)
     check_root && \
     run_latex && \
     run_dvips &&
     gzip -f "$FILEBASE.ps"
-    RC=$?
+    RC="$?"
     ;;
   pdf)
     check_root && \
     run_pdflatex
-    RC=$?
+    RC="$?"
     ;;
   bbl)
     check_root && \
     run_bibtex
-    RC=$?
+    RC="$?"
     ;;
   png)
     check_root && \
     run_thumbpdf
-    RC=$?
+    RC="$?"
     ;;
   sty)
     update_styles
-    RC=$?
+    RC="$?"
     ;;
   *)
     fail "Bad output format '$OUTFORMAT'"
     ;;
 esac
 
-exit $RC
+exit "$RC"
--- a/lib/Tools/logo	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/logo	Fri Sep 01 17:50:36 2000 +0200
@@ -1,11 +1,13 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: create an instance of the Isabelle logo
 
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -56,9 +58,9 @@
 # args
 
 NAME="-"
-[ $# -ge 1 ] && { NAME="$1"; shift; }
+[ "$#" -ge 1 ] && { NAME="$1"; shift; }
 
-[ $# -ne 0 -o "$NAME" = "-" ] && usage
+[ "$#" -ne 0 -o "$NAME" = "-" ] && usage
 
 
 ## main
@@ -73,8 +75,8 @@
 AUTO_PERL=perl
 
 if [ "$OUTFILE" = "-" ]; then
-  $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps
+  "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps"
 else
   [ -z "$QUIET" ] && echo "$OUTFILE" >&2
-  $AUTO_PERL -p -e "s/<any>/$NAME/" $ISABELLE_HOME/lib/logo/isabelle_any.eps > $OUTFILE
+  "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" > "$OUTFILE"
 fi
--- a/lib/Tools/make	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/make	Fri Sep 01 17:50:36 2000 +0200
@@ -1,11 +1,13 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: Isabelle make utility
 
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
--- a/lib/Tools/makeall	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/makeall	Fri Sep 01 17:50:36 2000 +0200
@@ -1,6 +1,8 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: apply make utility to all logics
 
@@ -11,7 +13,7 @@
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -36,10 +38,10 @@
 
 for L in $ALL_LOGICS
 do
-  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make "$@" )
+  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" )
 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/Tools/mkdir	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/mkdir	Fri Sep 01 17:50:36 2000 +0200
@@ -1,13 +1,15 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: prepare logic session directory
 
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -69,10 +71,10 @@
 # args
 
 
-if [ $# -eq 1 ]; then
+if [ "$#" -eq 1 ]; then
   LOGIC="$ISABELLE_LOGIC"
   DIR_NAME="$1"; shift
-elif [ $# -eq 2 ]; then
+elif [ "$#" -eq 2 ]; then
   LOGIC="$1"; shift
   DIR_NAME="$1"; shift
 else
--- a/lib/Tools/nonascii	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/nonascii	Fri Sep 01 17:50:36 2000 +0200
@@ -1,13 +1,15 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: check files for non-ASCII characters
 
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -22,9 +24,9 @@
 
 ## process command line
 
-[ $# -eq 0 -o "$1" = "-?" ] && usage
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
 
-SPECS="$@"; shift $#
+SPECS="$@"; shift "$#"
 
 
 ## main
@@ -33,5 +35,5 @@
 AUTO_PERL=perl
 
 find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
-  xargs $AUTO_PERL -w -e \
+  xargs "$AUTO_PERL" -w -e \
     'while(<ARGV>) { if (m/[\x80-\xff]/) { print "$ARGV: $_"; }}'
--- a/lib/Tools/symbolinput	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/symbolinput	Fri Sep 01 17:50:36 2000 +0200
@@ -1,10 +1,12 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: translate symbols into \<...> sequences
 
 #set by configure
 AUTO_PERL=perl
 
-exec $AUTO_PERL -w $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
+exec "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/symbolinput.pl" "$@"
--- a/lib/Tools/usedir	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/usedir	Fri Sep 01 17:50:36 2000 +0200
@@ -1,13 +1,15 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: build object-logic or run examples
 
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -92,12 +94,12 @@
 
 # args
 
-[ $# -ne 2 ] && usage
+[ "$#" -ne 2 ] && usage
 
 LOGIC="$1"; shift
 NAME="$1"; shift
 
-[ -z "$SESSION" ] && SESSION=$(basename $NAME)
+[ -z "$SESSION" ] && SESSION=$(basename "$NAME")
 
 
 
@@ -105,10 +107,10 @@
 
 # prepare browser info dir
 
-if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then
-  mkdir -p $ISABELLE_BROWSER_INFO
-  cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/isabelle.gif
-  cp $ISABELLE_HOME/lib/html/index.html $ISABELLE_BROWSER_INFO/index.html
+if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
+  mkdir -p "$ISABELLE_BROWSER_INFO"
+  cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
+  cp "$ISABELLE_HOME/lib/html/index.html" "$ISABELLE_BROWSER_INFO/index.html"
 fi
 
 
@@ -126,7 +128,7 @@
 
 if [ "$DOCUMENT" != false -a -d document ]; then
   DOC="$DOCUMENT"
-  [ -n "$DUMP" -a -d "$DUMP" ] && $ISATOOL latex -o sty "$DUMP/root.tex" >/dev/null
+  [ -n "$DUMP" -a -d "$DUMP" ] && "$ISATOOL" latex -o sty "$DUMP/root.tex" >/dev/null
 else
   DOC=""
 fi
@@ -142,34 +144,34 @@
   OPT_C=""
   [ "$COMPRESS" = true ] && OPT_C="-c"
 
-  $ISABELLE \
+  "$ISABELLE" \
     -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\";" \
-    $OPT_C -q -w $LOGIC $NAME > $LOG 2>&1
-  RC=$?
+    $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1
+  RC="$?"
 else
-  ITEM=$(basename $LOGIC)-"$SESSION"
+  ITEM=$(basename "$LOGIC")-"$SESSION"
   echo "Running $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
-  $ISABELLE \
+  "$ISABELLE" \
     -e "Session.use_dir $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\"; quit();" \
-    -r -q $LOGIC > $LOG 2>&1
-  RC=$?
+    -r -q "$LOGIC" > "$LOG" 2>&1
+  RC="$?"
   cd ..
 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"
isabelle