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

--- a/bin/isabelle	Fri Sep 01 17:45:07 2000 +0200
+++ b/bin/isabelle	Fri Sep 01 17:47:20 2000 +0200
@@ -1,16 +1,18 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # Basic Isabelle startup script.
 
 
 ## settings
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
-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; }
 
 
@@ -102,17 +104,17 @@
 INPUT=""
 OUTPUT=""
 
-if [ $# -ge 1 ]; then
+if [ "$#" -ge 1 ]; then
   INPUT="$1"
   shift
 fi
 
-if [ $# -ge 1 ]; then
+if [ "$#" -ge 1 ]; then
   OUTPUT="$1"
   shift
 fi
 
-[ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
+[ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
 
 
 ## check ML system
@@ -133,19 +135,22 @@
     [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\""
     ;;
   *)
+    INFILE=""
     ISA_PATH=""
-    INFILE=""
-    for DIR in $(echo $ISABELLE_PATH | tr : " ")
+
+    ORIG_IFS="$IFS"
+    IFS=":"
+    for DIR in $ISABELLE_PATH
     do
-      ISA_PATH="$ISA_PATH $DIR"
-      [ -z "$INFILE" -a -f $DIR/$INPUT ] && INFILE=$DIR/$INPUT
+      DIR="$DIR/$ML_IDENTIFIER"
+      ISA_PATH="$ISA_PATH  $DIR\n"
+      [ -z "$INFILE" -a -f "$DIR/$INPUT" ] && INFILE="$DIR/$INPUT"
     done
+    IFS="$ORIG_IFS"
+
     if [ -z "$INFILE" ]; then
       echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2
-      for DIR in $ISA_PATH
-      do
-        echo "  $DIR" >&2
-      done
+      echo -ne "$ISA_PATH" >&2
       exit 2
     fi
     ;;
@@ -178,20 +183,20 @@
 
 ## run it!
 
-ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
+ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
 
 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
 
 export INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP
 
-if [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ]; then
-  $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
+if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
+  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
 else
-  $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
+  "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
 fi
-RC=$?
+RC="$?"
 
 #Do not even think of 'rm -r'!!
-rmdir $ISABELLE_TMP
+rmdir "$ISABELLE_TMP"
 
-exit $RC
+exit "$RC"

--- a/bin/isatool	Fri Sep 01 17:45:07 2000 +0200
+++ b/bin/isatool	Fri Sep 01 17:47:20 2000 +0200
@@ -1,24 +1,24 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
-# Isabelle tool starter -- provides settings environment,
-#   and keeps your PATH name space clean.
+# Isabelle tool starter -- provides settings environment
+# and keeps your PATH name space clean.
 
 
 ## settings
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
-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; }
 
 
 ## diagnostics
 
-TOOLDIRS=$(echo $ISABELLE_TOOLS | tr : " ")
-
 function usage()
 {
   echo
@@ -29,9 +29,11 @@
   echo
   echo "  Available tools are:"
   (
-    for DIR in $TOOLDIRS
+    ORIG_IFS="$IFS"
+    IFS=":"
+    for DIR in $ISABELLE_TOOLS
     do
-      cd $DIR
+      cd "$DIR"
       echo
       for T in *
       do
@@ -41,6 +43,7 @@
         fi
       done
     done
+    IFS="$ORIG_IFS"
   )
   echo
   exit 1
@@ -55,7 +58,7 @@
 
 ## args
 
-[ $# -lt 1 -o "$1" = "-?" ] && usage
+[ "$#" -lt 1 -o "$1" = "-?" ] && usage
 
 TOOLNAME="$1"
 shift
@@ -63,10 +66,13 @@
 
 ## main
 
-for DIR in $TOOLDIRS
+ORIG_IFS="$IFS"
+IFS=":"
+for DIR in $ISABELLE_TOOLS
 do
-  TOOL=$DIR/$TOOLNAME
+  TOOL="$DIR/$TOOLNAME"
   [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
 done
+IFS="$ORIG_IFS"
 
 fail "Unknown Isabelle tool: $TOOLNAME"