--- a/Admin/ProofGeneral/3.7.1.1/interface Fri Oct 31 17:01:54 2014 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,262 +0,0 @@
-#!/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