--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/interface Thu Nov 26 12:55:24 2009 +0100
@@ -0,0 +1,252 @@
+#!/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
+
+ 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