diff -r 4030fcc5c785 -r b9357f56fd64 Admin/ProofGeneral/interface --- a/Admin/ProofGeneral/interface Fri Jan 28 11:26:08 2011 +1100 +++ /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