diff options
author | Makarius Wenzel <makarius@sketis.net> | 2005-09-17 11:12:42 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 2005-09-17 11:12:42 +0000 |
commit | 133e32197a6b68df8a04e32f95a90adc9b653ce3 (patch) | |
tree | 1b23b1b9fe9c5e66ab8154337eb1df3d91e4c2db | |
parent | 5306636f1baafb513df058260493f7a80fddfc43 (diff) |
removed (again) -- may use isar/interface -I false instead;
-rw-r--r-- | isa/interface | 247 |
1 files changed, 0 insertions, 247 deletions
diff --git a/isa/interface b/isa/interface deleted file mode 100644 index 94668f43..00000000 --- a/isa/interface +++ /dev/null @@ -1,247 +0,0 @@ -#!/usr/bin/env bash -# -# $Id$ -# -# Proof General interface wrapper for Isabelle. - - -## self references - -THIS=$(cd "$(dirname "$0")"; pwd) -SUPER=$(cd "$THIS/.."; pwd) -KIND=$(basename "$(dirname "$0")") - -if [ "$KIND" = isar ]; then - ISAR=true -else - ISAR=false -fi - - -## diagnostics - -usage() -{ - echo - echo "Usage: Isabelle [OPTIONS] [FILES ...]" - echo - echo " Options are:" - echo " -I BOOL use Isabelle/Isar instead of classic Isabelle (default $ISAR)" - 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 false)" - 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="" -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 -} - -getoptions $PROOFGENERAL_OPTIONS - -getoptions "$@" -shift $(($OPTIND - 1)) - -if [ "$ISAR" = true ]; then - KIND=isar - DEFAULT_FILES="Scratch.thy" -else - KIND=isa - DEFAULT_FILES="Scratch.thy Scratch.ML" -fi - - -# args - -if [ "$#" -eq 0 ]; then - FILES="$DEFAULT_FILES" -else - FILES="" - 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 - -if [ "$START_PG" = false ]; then - - [ "$ISAR" = true ] && ISABELLE_OPTIONS="$ISABELLE_OPTIONS -I" - exec "$ISABELLE" $ISABELLE_OPTIONS "$LOGIC" - -else - - ARGS="" - - [ -n "$GEOMETRY" ] && ARGS="$ARGS -geometry '$GEOMETRY'" - - [ "$INITFILE" = false ] && ARGS="$ARGS -q" - - if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then - [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts - else - ARGS="$ARGS -nw" - XSYMBOL=false - fi - - ARGS="$ARGS -l '$SUPER/isa/interface-setup.el'" - - if [ -n "$KEYWORDS" ]; then - if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then - ARGS="$ARGS -l '$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el'" - elif [ -f "$ISABELLE_HOME/etc/isar-keywords-$KEYWORDS.el" ]; then - ARGS="$ARGS -l '$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 '$ISABELLE_HOME_USER/etc/isar-keywords.el'" - elif [ -f "$ISABELLE_HOME/etc/isar-keywords.el" ]; then - ARGS="$ARGS -l '$ISABELLE_HOME/etc/isar-keywords.el'" - fi - - for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \ - "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el" - do - [ -f "$FILE" ] && ARGS="$ARGS -l '$FILE'" - done - - case "$LOGIC" in - /*) - ;; - */*) - LOGIC="$(pwd -P)/$LOGIC" - ;; - esac - - export PROOFGENERAL_HOME="$SUPER" - export PROOFGENERAL_ASSISTANTS="$KIND" - export PROOFGENERAL_LOGIC="$LOGIC" - export PROOFGENERAL_XSYMBOL="$XSYMBOL" - export PROOFGENERAL_UNICODE="$UNICODE" - - export ISABELLE_OPTIONS XSYMBOL_FONTSIZE - - eval exec "$PROGNAME" "$ARGS" "$FILES" - -fi |