1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/Admin/ProofGeneral/interface Thu Nov 26 12:55:24 2009 +0100
1.3 @@ -0,0 +1,252 @@
1.4 +#!/usr/bin/env bash
1.5 +#
1.6 +# interface,v 9.1 2008/02/06 15:40:45 makarius Exp
1.7 +#
1.8 +# Proof General interface wrapper for Isabelle.
1.9 +
1.10 +
1.11 +## self references
1.12 +
1.13 +THIS="$(cd "$(dirname "$0")"; pwd)"
1.14 +SUPER="$(cd "$THIS/.."; pwd)"
1.15 +
1.16 +
1.17 +## diagnostics
1.18 +
1.19 +usage()
1.20 +{
1.21 + echo
1.22 + echo "Usage: Isabelle [OPTIONS] [FILES ...]"
1.23 + echo
1.24 + echo " Options are:"
1.25 + echo " -I BOOL use Isabelle/Isar (default: true, implied by -P true)"
1.26 + echo " -L NAME abbreviates -l NAME -k NAME"
1.27 + echo " -P BOOL actually start Proof General (default true), otherwise"
1.28 + echo " run plain tty session"
1.29 + echo " -U BOOL enable Unicode (UTF-8) communication (default true)"
1.30 + echo " -X BOOL configure the X-Symbol package on startup (default true)"
1.31 + echo " -f SIZE set X-Symbol font size (default 12)"
1.32 + echo " -g GEOMETRY specify Emacs geometry"
1.33 + echo " -k NAME use specific isar-keywords for named logic"
1.34 + echo " -l NAME logic image name (default \$ISABELLE_LOGIC=$ISABELLE_LOGIC)"
1.35 + echo " -m MODE add print mode for output"
1.36 + echo " -p NAME Emacs program name (default emacs)"
1.37 + echo " -u BOOL use personal .emacs file (default true)"
1.38 + echo " -w BOOL use window system (default true)"
1.39 + echo " -x BOOL enable the X-Symbol package on startup (default false)"
1.40 + echo
1.41 + echo "Starts Proof General for Isabelle with theory and proof FILES"
1.42 + echo "(default Scratch.thy)."
1.43 + echo
1.44 + echo " PROOFGENERAL_OPTIONS=$PROOFGENERAL_OPTIONS"
1.45 + echo
1.46 + exit 1
1.47 +}
1.48 +
1.49 +fail()
1.50 +{
1.51 + echo "$1" >&2
1.52 + exit 2
1.53 +}
1.54 +
1.55 +
1.56 +## process command line
1.57 +
1.58 +# options
1.59 +
1.60 +ISABELLE_OPTIONS=""
1.61 +ISAR="true"
1.62 +START_PG="true"
1.63 +GEOMETRY=""
1.64 +KEYWORDS=""
1.65 +LOGIC="$ISABELLE_LOGIC"
1.66 +PROGNAME="emacs"
1.67 +INITFILE="true"
1.68 +WINDOWSYSTEM="true"
1.69 +XSYMBOL=""
1.70 +XSYMBOL_SETUP=true
1.71 +XSYMBOL_FONTSIZE="12"
1.72 +UNICODE=""
1.73 +
1.74 +getoptions()
1.75 +{
1.76 + OPTIND=1
1.77 + while getopts "I:L:P:U:X:f:g:k:l:m:p:u:w:x:" OPT
1.78 + do
1.79 + case "$OPT" in
1.80 + I)
1.81 + ISAR="$OPTARG"
1.82 + ;;
1.83 + L)
1.84 + KEYWORDS="$OPTARG"
1.85 + LOGIC="$OPTARG"
1.86 + ;;
1.87 + P)
1.88 + START_PG="$OPTARG"
1.89 + ;;
1.90 + U)
1.91 + UNICODE="$OPTARG"
1.92 + ;;
1.93 + X)
1.94 + XSYMBOL_SETUP="$OPTARG"
1.95 + ;;
1.96 + f)
1.97 + XSYMBOL_FONTSIZE="$OPTARG"
1.98 + ;;
1.99 + g)
1.100 + GEOMETRY="$OPTARG"
1.101 + ;;
1.102 + k)
1.103 + KEYWORDS="$OPTARG"
1.104 + ;;
1.105 + l)
1.106 + LOGIC="$OPTARG"
1.107 + ;;
1.108 + m)
1.109 + if [ -z "$ISABELLE_OPTIONS" ]; then
1.110 + ISABELLE_OPTIONS="-m $OPTARG"
1.111 + else
1.112 + ISABELLE_OPTIONS="$ISABELLE_OPTIONS -m $OPTARG"
1.113 + fi
1.114 + ;;
1.115 + p)
1.116 + PROGNAME="$OPTARG"
1.117 + ;;
1.118 + u)
1.119 + INITFILE="$OPTARG"
1.120 + ;;
1.121 + w)
1.122 + WINDOWSYSTEM="$OPTARG"
1.123 + ;;
1.124 + x)
1.125 + XSYMBOL="$OPTARG"
1.126 + ;;
1.127 + \?)
1.128 + usage
1.129 + ;;
1.130 + esac
1.131 + done
1.132 +}
1.133 +
1.134 +eval "OPTIONS=($PROOFGENERAL_OPTIONS)"
1.135 +getoptions "${OPTIONS[@]}"
1.136 +
1.137 +getoptions "$@"
1.138 +shift $(($OPTIND - 1))
1.139 +
1.140 +
1.141 +# args
1.142 +
1.143 +declare -a FILES=()
1.144 +
1.145 +if [ "$#" -eq 0 ]; then
1.146 + FILES["${#FILES[@]}"]="Scratch.thy"
1.147 +else
1.148 + while [ "$#" -gt 0 ]; do
1.149 + FILES["${#FILES[@]}"]="$1"
1.150 + shift
1.151 + done
1.152 +fi
1.153 +
1.154 +
1.155 +## smart X11 font installation
1.156 +
1.157 +function checkfonts ()
1.158 +{
1.159 + XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1
1.160 +
1.161 + case "$XLSFONTS" in
1.162 + xlsfonts:*)
1.163 + return 1
1.164 + ;;
1.165 + esac
1.166 +
1.167 + return 0
1.168 +}
1.169 +
1.170 +function installfonts ()
1.171 +{
1.172 + checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS
1.173 +}
1.174 +
1.175 +
1.176 +## main
1.177 +
1.178 +# Isabelle2008 compatibility
1.179 +[ -z "$ISABELLE_PROCESS" ] && export ISABELLE_PROCESS="$ISABELLE"
1.180 +[ -z "$ISABELLE_TOOL" ] && export ISABELLE_TOOL="$ISATOOL"
1.181 +
1.182 +if [ "$START_PG" = false ]; then
1.183 +
1.184 + [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I"
1.185 + exec "$ISABELLE_PROCESS" $ISABELLE_OPTIONS "$LOGIC"
1.186 +
1.187 +else
1.188 +
1.189 + declare -a ARGS=()
1.190 +
1.191 + if [ -n "$GEOMETRY" ]; then
1.192 + ARGS["${#ARGS[@]}"]="-geometry"
1.193 + ARGS["${#ARGS[@]}"]="$GEOMETRY"
1.194 + fi
1.195 +
1.196 + [ "$INITFILE" = false ] && ARGS["${#ARGS[@]}"]="-q"
1.197 +
1.198 + if [ "$WINDOWSYSTEM" = false ]; then
1.199 + ARGS["${#ARGS[@]}"]="-nw"
1.200 + XSYMBOL=false
1.201 + elif [ -z "$DISPLAY" ]; then
1.202 + XSYMBOL=false
1.203 + else
1.204 + [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts
1.205 + fi
1.206 +
1.207 + ARGS["${#ARGS[@]}"]="-l"
1.208 + ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el"
1.209 +
1.210 + if [ -n "$KEYWORDS" ]; then
1.211 + if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then
1.212 + ARGS["${#ARGS[@]}"]="-l"
1.213 + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el"
1.214 + elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then
1.215 + ARGS["${#ARGS[@]}"]="-l"
1.216 + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el"
1.217 + else
1.218 + fail "No isar-keywords file for '$KEYWORDS'"
1.219 + fi
1.220 + elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then
1.221 + ARGS["${#ARGS[@]}"]="-l"
1.222 + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el"
1.223 + elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
1.224 + ARGS["${#ARGS[@]}"]="-l"
1.225 + ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el"
1.226 + fi
1.227 +
1.228 + for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
1.229 + "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
1.230 + do
1.231 + if [ -f "$FILE" ]; then
1.232 + ARGS["${#ARGS[@]}"]="-l"
1.233 + ARGS["${#ARGS[@]}"]="$FILE"
1.234 + fi
1.235 + done
1.236 +
1.237 + case "$LOGIC" in
1.238 + /*)
1.239 + ;;
1.240 + */*)
1.241 + LOGIC="$(pwd -P)/$LOGIC"
1.242 + ;;
1.243 + esac
1.244 +
1.245 + export PROOFGENERAL_HOME="$SUPER"
1.246 + export PROOFGENERAL_ASSISTANTS="isar"
1.247 + export PROOFGENERAL_LOGIC="$LOGIC"
1.248 + export PROOFGENERAL_XSYMBOL="$XSYMBOL"
1.249 + export PROOFGENERAL_UNICODE="$UNICODE"
1.250 +
1.251 + export ISABELLE_OPTIONS XSYMBOL_FONTSIZE
1.252 +
1.253 + exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}"
1.254 +
1.255 +fi