# HG changeset patch # User wenzelm # Date 857145391 -3600 # Node ID afa01c9f1ab04430f94ae4a2d0bc4e7861547076 # Parent 5ce1310560ffa960fb96703182e460b75d1ad44e more robust handling of invocation errors; added -m MODE option; diff -r 5ce1310560ff -r afa01c9f1ab0 bin/isabelle --- a/bin/isabelle Fri Feb 28 16:55:35 1997 +0100 +++ b/bin/isabelle Fri Feb 28 16:56:31 1997 +0100 @@ -7,14 +7,27 @@ ## settings +PRG=$(basename $0) + ISABELLE_HOME=$(dirname $(dirname $0)) -. $ISABELLE_HOME/lib/scripts/getsettings || exit 2 +case "$ISABELLE_HOME" in + /*) + if [ -f $ISABELLE_HOME/lib/scripts/getsettings ]; then + . $ISABELLE_HOME/lib/scripts/getsettings || exit 2 + else + echo "ERROR: $PRG probably not called from its original place!" + exit 1 + fi + ;; + *) + echo "ERROR: $PRG not called with absolute path specification!" + exit 1 + ;; +esac ## diagnostics -PRG=$(basename $0) - function usage() { echo @@ -23,6 +36,7 @@ echo " Options are:" echo " -c force copying of heap file (for Poly/ML)" echo " -e MLTEXT pass MLTEXT to the ML session" + echo " -m MODE add print mode for output" echo " -q non-interactive session" echo " -r open heap file read-only" echo " -u pass 'exit_use_dir\".\";' to the ML session" @@ -49,10 +63,11 @@ COPYDB="" MLTEXT="" COPYDB="" +MODES="" TERMINATE="" READONLY="" -while getopts "ce:qru" OPT +while getopts "ce:m:qru" OPT do case "$OPT" in c) @@ -61,6 +76,13 @@ e) MLTEXT="$MLTEXT $OPTARG" ;; + m) + if [ -z "$MODES" ]; then + MODES="\"$OPTARG\"" + else + MODES="$MODES, \"$OPTARG\"" + fi + ;; q) TERMINATE=true ;; @@ -155,6 +177,8 @@ ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-) +[ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT" + export INFILE OUTFILE COPYDB MLTEXT TERMINATE [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE