diff options
author | Makarius Wenzel <makarius@sketis.net> | 1999-04-16 16:15:27 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 1999-04-16 16:15:27 +0000 |
commit | 9bafbd1b551c9cf8d7c3a7fb96511966ed094831 (patch) | |
tree | 05cbcb8b6ee845e4d77285ee6bf3d3cf9849b9c0 /isar/interface | |
parent | 9d69d66256b4c88c89fb3903de29bc71b2fb36cb (diff) |
initial version of 'isar proof assistant (Isabelle/Isar);
Diffstat (limited to 'isar/interface')
-rw-r--r-- | isar/interface | 108 |
1 files changed, 108 insertions, 0 deletions
diff --git a/isar/interface b/isar/interface new file mode 100644 index 00000000..e294799d --- /dev/null +++ b/isar/interface @@ -0,0 +1,108 @@ +#!/bin/bash +# +# $Id$ +# +# ProofGeneral interface wrapper for Isabelle/Isar. + + +## diagnostics + +PRG=$(basename $0) + +function usage() +{ + echo + echo "Usage: $PRG [OPTIONS] [FILES ...]" + echo + echo " Options are:" + echo " -l NAME logic image name (default $ISABELLE_LOGIC)" + echo " -p NAME Emacs program name (default xemacs)" + echo " -u BOOL use .emacs file (default false)" + echo " -w BOOL use window system (default true)" + echo + echo "Starts ProofGeneral for Isabelle/Isar with LOGIC images and theory FILES." + exit 1 +} + +function fail() +{ + echo "$1" >&2 + exit 2 +} + + +## process command line + +PG_HOME=$(cd $(dirname "$0"); cd ..; echo $PWD) + + +# options + +LOGIC="$ISABELLE_LOGIC" +PROGNAME="xemacs" +INITFILE="false" +WINDOWSYSTEM="true" + +function getoptions() +{ + OPTIND=1 + while getopts "l:p:u:w:" OPT + do + case "$OPT" in + l) + LOGIC="$OPTARG" + ;; + p) + PROGNAME="$OPTARG" + ;; + u) + INITFILE="$OPTARG" + ;; + w) + WINDOWSYSTEM="$OPTARG" + ;; + \?) + usage + ;; + esac + done +} + +getoptions $PROOFGENERAL_OPTIONS + +getoptions "$@" +shift $(($OPTIND - 1)) + + +# args + +FILES="$@" +shift $# + +[ -z "$FILES" ] && FILES="Scratch.thy" + + +## main + +ARGS="" + +[ "$INITFILE" = false ] && ARGS="$ARGS -q" + +if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then + ARGS="$ARGS -T Isabelle" +else + ARGS="$ARGS -nw" +fi + + +ARGS="$ARGS -l $PG_HOME/isar/interface-setup.el -l $PG_HOME/generic/proof-site.el" + +for FILE in "$ISABELLE_HOME/etc/proofgeneral-settings.el" \ + "$ISABELLE_HOME_USER/etc/proofgeneral-settings.el" +do + [ -f "$FILE" ] && ARGS="$ARGS -l $FILE" +done + +export PROOFGENERAL_HOME="$PG_HOME/" +export PROOFGENERAL_LOGIC="$LOGIC" +exec $PROGNAME $ARGS $FILES |