#!/bin/sh
#
# $Id$
#
# Proof General interface wrapper for Isabelle.

## self references

THIS=`cd \`dirname "$0"\`; pwd`
SUPER=`cd "$THIS/.."; pwd`
KIND=`basename \`dirname "$0"\``

if [ "$KIND" = isar ]; then
  ISAR=true
else
  ISAR=false
fi


## diagnostics

usage()
{
  echo
  echo "Usage: Isabelle [OPTIONS] [FILES ...]"
  echo
  echo "  Options are:"
  echo "    -I BOOL      use Isabelle/Isar instead of classic Isabelle (default $ISAR)"
  echo "    -X BOOL      configure the X-Symbol package on startup (default true)"
  echo "    -l NAME      logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
  echo "    -p NAME      Emacs program name (default xemacs)"
  echo "    -u BOOL      use personal .emacs file (default true)"
  echo "    -w BOOL      use window system (default true)"
  echo "    -x BOOL      enable the X-Symbol package on startup (default false)"
  echo
  echo "Starts Proof General for Isabelle with theory and proof FILES"
  echo "(default Scratch.thy)."
  echo
  echo "  PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS"
  echo
  exit 1
}

fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

LOGIC="$ISABELLE_LOGIC"
PROGNAME="xemacs"
INITFILE="true"
WINDOWSYSTEM="true"
XSYMBOL=""
XSYMBOLSETUP=true

getoptions()
{
  OPTIND=1
  while getopts "I:X:l:p:u:w:x:" OPT
  do
    case "$OPT" in
      I)
        ISAR="$OPTARG"
        ;;
      X)
        XSYMBOLSETUP="$OPTARG"
        ;;
      l)
        LOGIC="$OPTARG"
        ;;
      p)
        PROGNAME="$OPTARG"
        ;;
      u)
        INITFILE="$OPTARG"
        ;;
      w)
        WINDOWSYSTEM="$OPTARG"
        ;;
      x)
        XSYMBOL="$OPTARG"
        ;;
      \?)
        usage
        ;;
    esac
  done
}

getoptions $PROOFGENERAL_OPTIONS

getoptions $*
shift `expr $OPTIND - 1`

if [ "$ISAR" = true ]; then
  KIND=isar
  DEFAULT_FILES="Scratch.thy"
else
  KIND=isa
  DEFAULT_FILES="Scratch.thy Scratch.ML"
fi


# args

FILES="$@"
shift "$#"

[ -z "$FILES" ] && FILES="$DEFAULT_FILES"


## main

ARGS=""

[ "$INITFILE" = false ] && ARGS="$ARGS -q"

if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then
  ARGS="$ARGS -T Isabelle"
  [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOLSETUP" = true ] && "$ISATOOL" installfonts -x
else
  ARGS="$ARGS -nw"
  XSYMBOL=false
fi

[ ! "$XSYMBOLSETUP" = true ] && XSYMBOL_HOME=""


ARGS="$ARGS -l $SUPER/isa/interface-setup.el"

for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
    "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
do
  [ -f "$FILE" ] && ARGS="$ARGS -l $FILE"
done

PROOFGENERAL_HOME="$SUPER"
PROOFGENERAL_ASSISTANTS="$KIND"
PROOFGENERAL_LOGIC="$LOGIC"
PROOFGENERAL_XSYMBOL="$XSYMBOL"

export PROOFGENERAL_HOME PROOFGENERAL_ASSISTANTS PROOFGENERAL_LOGIC PROOFGENERAL_XSYMBOL

exec $PROGNAME $ARGS $FILES