#!/bin/bash

 #

 # $Id$

 #

 # Basic Isabelle startup script.

 ## 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! Unable to run Isabelle."

 ## input heap file

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

 case "$INPUT" in

   SYSTEM)

     INFILE=""

     ;;

   */*)

     INFILE="$INPUT"

     [ ! -f "$INFILE" ] && fail "Bad heap file file: \"$INFILE\""

     ;;

   *)

     ISA_PATH=""

     INFILE=""

     for DIR in $(echo $ISABELLE_PATH | tr : " ")

     do

       ISA_PATH="$ISA_PATH $DIR/$ML_SYSTEM-$PLATFORM"

       [ -z "$INFILE" -a -f $DIR/$ML_SYSTEM-$PLATFORM/$INPUT ] && INFILE=$DIR/$ML_SYSTEM-$PLATFORM/$INPUT

     done

     if [ -z "$INFILE" ]; then

       echo "Unknown logic \"$INPUT\" -- no heap file found in:"

       for DIR in $ISA_PATH

       do

         echo "  $DIR"

       done

       exit 2

     fi

     ;;

 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