#!/usr/bin/env bash

#

# interface,v 9.1 2008/02/06 15:40:45 makarius Exp

#

# Proof General interface wrapper for Isabelle.

## self references

THIS="$(cd "$(dirname "$0")"; pwd)"

SUPER="$(cd "$THIS/.."; pwd)"

## diagnostics

usage()

{

  echo

  echo "Usage: Isabelle [OPTIONS] [FILES ...]"

  echo

  echo "  Options are:"

  echo "    -I BOOL      use Isabelle/Isar (default: true, implied by -P true)"

  echo "    -L NAME      abbreviates -l NAME -k NAME"

  echo "    -P BOOL      actually start Proof General (default true), otherwise"

  echo "                 run plain tty session"

  echo "    -U BOOL      enable Unicode (UTF-8) communication (default true)"

  echo "    -X BOOL      configure the X-Symbol package on startup (default true)"

  echo "    -f SIZE      set X-Symbol font size (default 12)"

  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 emacs)"

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

ISAR="true"

START_PG="true"

GEOMETRY=""

KEYWORDS=""

LOGIC="$ISABELLE_LOGIC"

PROGNAME="emacs"

INITFILE="true"

WINDOWSYSTEM="true"

XSYMBOL=""

XSYMBOL_SETUP=true

XSYMBOL_FONTSIZE="12"

UNICODE=""

getoptions()

{

  OPTIND=1

  while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT

  do

    case "$OPT" in

      I)

        ISAR="$OPTARG"

        ;;

      L)

        KEYWORDS="$OPTARG"

        LOGIC="$OPTARG"

        ;;

      P)

        START_PG="$OPTARG"

        ;;

      U)

        UNICODE="$OPTARG"

        ;;

      X)

        XSYMBOL_SETUP="$OPTARG"

        ;;

      f)

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

}

eval "OPTIONS=($PROOFGENERAL_OPTIONS)"

getoptions "${OPTIONS[@]}"

getoptions "$@"

shift $(($OPTIND - 1))

# args

declare -a FILES=()

if [ "$#" -eq 0 ]; then

  FILES["${#FILES[@]}"]="Scratch.thy"

else

  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

# Isabelle2008 compatibility

[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE"

[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL"

if [ "$START_PG" = false ]; then

  [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"

  exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"

else

  declare -a ARGS=()

  if [ -n "$GEOMETRY" ]; then

    ARGS["${#ARGS[@]}"]="-geometry"

    ARGS["${#ARGS[@]}"]="$GEOMETRY"

  fi

  [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q"

  if [ "$WINDOWSYSTEM" = false ]; then

    ARGS["${#ARGS[@]}"]="-nw"

    XSYMBOL=false

  elif [ -z "$DISPLAY" ]; then

    XSYMBOL=false

  else

    [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts

  fi

  if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ]

  then

    if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ]

    then

      cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/"

      cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/"

      sleep 3

    fi

  fi

  ARGS["${#ARGS[@]}"]="-l"

  ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el"

  if [ -n "$KEYWORDS" ]; then

    if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then

      ARGS["${#ARGS[@]}"]="-l"

      ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el"

    elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then

      ARGS["${#ARGS[@]}"]="-l"

      ARGS["${#ARGS[@]}"]="$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"

    ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el"

  elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then

    ARGS["${#ARGS[@]}"]="-l"

    ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el"

  fi

  for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \

      "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"

  do

    if [ -f "$FILE" ]; then

      ARGS["${#ARGS[@]}"]="-l"

      ARGS["${#ARGS[@]}"]="$FILE"

    fi

  done

  case "$LOGIC" in

    /*)

      ;;

    */*)

      LOGIC="$(pwd -P)/$LOGIC"

      ;;

  esac

  export PROOFGENERAL_HOME="$SUPER"

  export PROOFGENERAL_ASSISTANTS="isar"

  export PROOFGENERAL_LOGIC="$LOGIC"

  export PROOFGENERAL_XSYMBOL="$XSYMBOL"

  export PROOFGENERAL_UNICODE="$UNICODE"

  export ISABELLE_OPTIONS XSYMBOL_FONTSIZE

  exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}"

fi