1.1 --- a/Admin/ProofGeneral/interface Thu Jan 27 17:37:42 2011 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,262 +0,0 @@
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 - if [ $(uname -s) = Darwin -a -d "$HOME/Library/Fonts" ]
1.208 - then
1.209 - if [ ! -f "$HOME/Library/Fonts/XSymb0Medium.ttf" -o ! -f "$HOME/Library/Fonts/XSymb1Medium.ttf" ]
1.210 - then
1.211 - cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf" "$HOME/Library/Fonts/"
1.212 - cp -f "$SUPER/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf" "$HOME/Library/Fonts/"
1.213 - sleep 3
1.214 - fi
1.215 - fi
1.216 -
1.217 - ARGS["${#ARGS[@]}"]="-l"
1.218 - ARGS["${#ARGS[@]}"]="$SUPER/isar/interface-setup.el"
1.219 -
1.220 - if [ -n "$KEYWORDS" ]; then
1.221 - if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then
1.222 - ARGS["${#ARGS[@]}"]="-l"
1.223 - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el"
1.224 - elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then
1.225 - ARGS["${#ARGS[@]}"]="-l"
1.226 - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el"
1.227 - else
1.228 - fail "No isar-keywords file for '$KEYWORDS'"
1.229 - fi
1.230 - elif [ -f "$ISABELLE_HOME_USER/etc/isar-keywords.el" ]; then
1.231 - ARGS["${#ARGS[@]}"]="-l"
1.232 - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME_USER/etc/isar-keywords.el"
1.233 - elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then
1.234 - ARGS["${#ARGS[@]}"]="-l"
1.235 - ARGS["${#ARGS[@]}"]="$ISABELLE_HOME/etc/isar-keywords.el"
1.236 - fi
1.237 -
1.238 - for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \
1.239 - "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el"
1.240 - do
1.241 - if [ -f "$FILE" ]; then
1.242 - ARGS["${#ARGS[@]}"]="-l"
1.243 - ARGS["${#ARGS[@]}"]="$FILE"
1.244 - fi
1.245 - done
1.246 -
1.247 - case "$LOGIC" in
1.248 - /*)
1.249 - ;;
1.250 - */*)
1.251 - LOGIC="$(pwd -P)/$LOGIC"
1.252 - ;;
1.253 - esac
1.254 -
1.255 - export PROOFGENERAL_HOME="$SUPER"
1.256 - export PROOFGENERAL_ASSISTANTS="isar"
1.257 - export PROOFGENERAL_LOGIC="$LOGIC"
1.258 - export PROOFGENERAL_XSYMBOL="$XSYMBOL"
1.259 - export PROOFGENERAL_UNICODE="$UNICODE"
1.260 -
1.261 - export ISABELLE_OPTIONS XSYMBOL_FONTSIZE
1.262 -
1.263 - exec "$PROGNAME" "${ARGS[@]}" "${FILES[@]}"
1.264 -
1.265 -fi