bin/isabelle

isabelle: Basic Isabelle startup script.

#!/bin/bash
#
# Basic Isabelle startup script.
#
# $Id$


## settings

ISABELLE_HOME=$(dirname $(dirname $0))
. $ISABELLE_HOME/lib/scripts/getsettings

#get bash-style platform info
unset HOSTTYPE
unset OSTYPE
PLATFORM=$(bash -noprofile -c 'echo $HOSTTYPE-$OSTYPE')


## diagnostics

PRG=$(basename $0)

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] [INPUT] [OUTPUT]"
  echo
  echo "  Options are:"
  echo "    -c           force copying of heap file"
  echo "    -e MLTEXT    pass MLTEXT to ML session"
#FIXME  echo "    -o OPTIONS   pass options to ML system"
  echo "    -q           non-interactive session"
  echo "    -r           open heap file read-only"
  echo "    -u           pass 'use\"ROOT.ML\" handle _ => exit 1; commit();'"
  echo "                 to the ML session"
  echo
  echo "  INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
  echo "  These are either names to be searched in the Isabelle path, or actual"
  echo "  file names (containing at least one /)."
  echo "  If INPUT is \"SYSTEM\", just start the bare bones ML system."
  echo
  exit 1
}

function fail()
{
  echo "$1"
  exit 2
}


## process command line

# options

COPYDB=""
MLTEXT=""
COPYDB=""
OPTIONS=""
TERMINATE=""
READONLY=""

while getopts "ce:qru" OPT
do
  case "$OPT" in
    c)
      COPYDB=true
      ;;
    e)
      MLTEXT="$MLTEXT $OPTARG"
      ;;
    o)
      OPTIONS="$OPTIONS $OPTARG"
      ;;
    q)
      TERMINATE=true
      ;;
    r)
      READONLY=true
      ;;
    u)
      MLTEXT="$MLTEXT use\"ROOT.ML\" handle _ => exit 1; commit();"
      ;;
    \?)
      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 ] && fail "Bad args: $*"


## check ML system

[ -z "$ML_SYSTEM" ] && fail "Missing ML system settings! Sorry, no Isabelle."


## input heap file

[ -z "$INPUT" ] && INPUT="$DEFAULT_LOGIC"

case "$INPUT" in
  SYSTEM)
    INFILE=""
    ;;
  */*)
    INFILE="$INPUT"
    [ ! -f "$INFILE" ] && fail "Bad heap file file: \"$INFILE\""
    ;;
  *)
    INFILE=""
    for DIR in $(echo $ISABELLE_PATH | tr : " ")
    do
      [ -z "$INFILE" -a -f $DIR/$ML_SYSTEM-$PLATFORM/$INPUT ] && INFILE=$DIR/$ML_SYSTEM-$PLATFORM/$INPUT
    done
    [ -z "$INFILE" ] && fail "Unknown logic: \"$INPUT\""
    ;;
esac


## output heap file

case "$OUTPUT" in
  "")
    [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
    ;;
  */*)
    OUTFILE="$OUTPUT"
    ;;
  *)
    OUTDIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM"
    mkdir -p "$OUTDIR"
    OUTFILE="$OUTDIR/$OUTPUT"
    ;;
esac


## run it!

ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)

export INFILE OUTFILE COPYDB MLTEXT OPTIONS 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