#!/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 "    -u           pass 'exit_use_dir\".\";' 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 (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:qru" 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

      ;;

    u)

      MLTEXT="$MLTEXT exit_use_dir\".\";"

      ;;

    \?)

      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="$DEFAULT_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