#!/usr/bin/env bash
#
# $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 "    -P BOOL      actually start Proof General (default true), otherwise"
  echo "                 run plain tty session"
  echo "    -X BOOL      configure the X-Symbol package on startup (default true)"
  echo "    -g GEOMETRY  specify Emacs geometry"
  echo "    -k NAME      use specific isar-keywords for named logic"
  echo "    -l NAME      logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
  echo "    -m MODE      add print mode for output"
  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

ISABELLE_OPTIONS=""
START_PG="true"
GEOMETRY=""
KEYWORDS=""
LOGIC="$ISABELLE_LOGIC"
PROGNAME="xemacs"
INITFILE="true"
WINDOWSYSTEM="true"
XSYMBOL=""
XSYMBOLSETUP=true

getoptions()
{
  OPTIND=1
  while getopts "I:P:X:g:k:l:m:p:u:w:x:" OPT
  do
    case "$OPT" in
      I)
        ISAR="$OPTARG"
        ;;
      P)
        START_PG="$OPTARG"
        ;;
      X)
        XSYMBOLSETUP="$OPTARG"
        ;;
      g)
        GEOMETRY="$OPTARG"
        ;;
      k)
        KEYWORDS="$OPTARG"
        ;;
      l)
        LOGIC="$OPTARG"
        ;;
      m)
        if [ -z "$ISABELLE_OPTIONS" ]; then
          ISABELLE_OPTIONS="-m $OPTARG"
        else
          ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG"
        fi
        ;;
      p)
        PROGNAME="$OPTARG"
        ;;
      u)
        INITFILE="$OPTARG"
        ;;
      w)
        WINDOWSYSTEM="$OPTARG"
        ;;
      x)
        XSYMBOL="$OPTARG"
        ;;
      \?)
        usage
        ;;
    esac
  done
}

getoptions $PROOFGENERAL_OPTIONS

getoptions "$@"
shift $(($OPTIND - 1))

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


# args

if [ "$#" -eq 0 ]; then
  FILES="$DEFAULT_FILES"
else
  FILES=""
  while [ "$#" -gt 0 ]; do
    FILES="$FILES '$1'"
    shift
  done
fi


## smart X11 font installation

function checkfonts ()
{
  XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1

  case "$XLSFONTS" in
    xlsfonts:*)
      return 1
      ;;
  esac

  return 0
}

function installfonts ()
{
  checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS
}


## main

if [ "$START_PG" = false ]; then

  [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"
  exec "$ISABELLE" $ISABELLE_OPTIONS "$LOGIC"

else

  ARGS=""

  [ -n "$GEOMETRY" ] && ARGS="$ARGS -geometry '$GEOMETRY'"

  [ "$INITFILE" = false ] && ARGS="$ARGS -q"
  
  if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then
    ARGS="$ARGS -T Isabelle"
    [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOLSETUP" = true ] && installfonts
  else
    ARGS="$ARGS -nw"
    XSYMBOL=false
  fi
  
  [ ! "$XSYMBOLSETUP" = true ] && XSYMBOL_HOME=""
  
  
  ARGS="$ARGS -l '$SUPER/isa/interface-setup.el'"

  if [ -n "$KEYWORDS" ]; then
    if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then
      ARGS="$ARGS -l '$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el'"
    elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then
      ARGS="$ARGS -l '$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el'"
    else
      fail "No isar-keywords file for '$KEYWORDS'"
    fi
  elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then
    ARGS="$ARGS -l '$ISABELLE_HOME_USER/etc/isar-keywords.el'"
  elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
    ARGS="$ARGS -l '$ISABELLE_HOME/etc/isar-keywords.el'"
  fi
  
  for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
      "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
  do
    [ -f "$FILE" ] && ARGS="$ARGS -l '$FILE'"
  done
  
  case "$LOGIC" in
    /*)
      ;;
    */*)
      LOGIC="$PWD/$LOGIC"
      ;;
  esac
  
  PROOFGENERAL_HOME="$SUPER"
  PROOFGENERAL_ASSISTANTS="$KIND"
  PROOFGENERAL_LOGIC="$LOGIC"
  PROOFGENERAL_XSYMBOL="$XSYMBOL"
  
  export PROOFGENERAL_HOME PROOFGENERAL_ASSISTANTS PROOFGENERAL_LOGIC PROOFGENERAL_XSYMBOL
  export ISABELLE_OPTIONS
  
  eval exec "$PROGNAME" "$ARGS" "$FILES"

fi