#!/usr/wiss/wenzelm/bin/bash # # $Id$ # # Basic Isabelle startup script. ## settings PRG=$(basename $0) ISABELLE_HOME=$(dirname $0)/.. . $ISABELLE_HOME/lib/scripts/getsettings || \ { echo "$PRG probably not called from its original place!"; exit 2; } ## diagnostics function usage() { echo echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]" echo echo " Options are:" 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 echo " INPUT (default \"$ISABELLE_LOGIC\") and OUTPUT specify in/out heaps." echo " These are either names to be searched in the Isabelle path, or actual" echo " file names (then containing at least one /)." echo " If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system." echo exit 1 } function fail() { echo "$1" >&2 exit 2 } ## process command line # options MLTEXT="" MODES="" TERMINATE="" READONLY="" while getopts "e:m:qr" OPT do case "$OPT" in e) MLTEXT="$MLTEXT $OPTARG" ;; m) if [ -z "$MODES" ]; then MODES="\"$OPTARG\"" else MODES="\"$OPTARG\", $MODES" fi ;; q) TERMINATE=true ;; r) READONLY=true ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args INPUT="" OUTPUT="" if [ $# -ge 1 ]; then INPUT="$1" shift fi if [ $# -ge 1 ]; then OUTPUT="$1" shift fi [ $# -ne 0 ] && { echo "Bad args: $*"; usage; } ## check ML system [ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Unable to run Isabelle." ## input heap file [ -z "$INPUT" ] && INPUT="$ISABELLE_LOGIC" case "$INPUT" in RAW_ML_SYSTEM) INFILE="" ;; */*) INFILE="$INPUT" [ ! -f "$INFILE" ] && fail "Bad heap file: \"$INFILE\"" ;; *) ISA_PATH="" INFILE="" for DIR in $(echo $ISABELLE_PATH | tr : " ") do ISA_PATH="$ISA_PATH $DIR" [ -z "$INFILE" -a -f $DIR/$INPUT ] && INFILE=$DIR/$INPUT done if [ -z "$INFILE" ]; then echo "Unknown logic \"$INPUT\" -- no heap file found in:" >&2 for DIR in $ISA_PATH do echo " $DIR" >&2 done exit 2 fi ;; esac ## output heap file case "$OUTPUT" in "") [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE" ;; */*) OUTFILE="$OUTPUT" ;; *) mkdir -p "$ISABELLE_OUTPUT" OUTFILE="$ISABELLE_OUTPUT/$OUTPUT" ;; esac ## run it! ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-) [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT" export INFILE OUTFILE 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