From 9bafbd1b551c9cf8d7c3a7fb96511966ed094831 Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Fri, 16 Apr 1999 16:15:27 +0000 Subject: initial version of 'isar proof assistant (Isabelle/Isar); --- isar/interface | 108 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 108 insertions(+) create mode 100644 isar/interface (limited to 'isar/interface') 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 -- cgit v1.2.3