Admin/ProofGeneral/interface

make sure short theorem names are preferred to composite ones in Sledgehammer;
this code used to work at some point

#!/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