diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2006-12-07 19:51:41 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2006-12-07 19:51:41 +0000 |
| commit | 91c7cb718f35c0fb4485cd6afe9c9529cd38d603 (patch) | |
| tree | c5c7d473f02b1fe4ee7d1a11da60711dea479400 /isar/interface | |
| parent | a4b24e4e30d10a79f3d8fc90d1acd69b80b4c2ab (diff) | |
removed obsolete references to 'isa';
Diffstat (limited to 'isar/interface')
| -rw-r--r-- | isar/interface | 24 |
1 files changed, 5 insertions, 19 deletions
diff --git a/isar/interface b/isar/interface index 8b835b6b..47af652f 100644 --- a/isar/interface +++ b/isar/interface @@ -9,13 +9,6 @@ THIS=$(cd "$(dirname "$0")"; pwd) SUPER=$(cd "$THIS/.."; pwd) -KIND=$(basename "$(dirname "$0")") - -if [ "$KIND" = isar ]; then - ISAR=true -else - ISAR=false -fi ## diagnostics @@ -26,7 +19,7 @@ usage() echo "Usage: Isabelle [OPTIONS] [FILES ...]" echo echo " Options are:" - echo " -I BOOL use Isabelle/Isar instead of classic Isabelle (default $ISAR)" + 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" @@ -62,6 +55,7 @@ fail() # options ISABELLE_OPTIONS="" +ISAR="true" START_PG="true" GEOMETRY="" KEYWORDS="" @@ -139,19 +133,11 @@ 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" + FILES="Scratch.thy" else FILES="" while [ "$#" -gt 0 ]; do @@ -204,7 +190,7 @@ else XSYMBOL=false fi - ARGS="$ARGS -l '$SUPER/isa/interface-setup.el'" + ARGS="$ARGS -l '$SUPER/isar/interface-setup.el'" if [ -n "$KEYWORDS" ]; then if [ -f "$ISABELLE_HOME_USER/etc/isar-keywords-$KEYWORDS.el" ]; then @@ -235,7 +221,7 @@ else esac export PROOFGENERAL_HOME="$SUPER" - export PROOFGENERAL_ASSISTANTS="$KIND" + export PROOFGENERAL_ASSISTANTS="isar" export PROOFGENERAL_LOGIC="$LOGIC" export PROOFGENERAL_XSYMBOL="$XSYMBOL" export PROOFGENERAL_UNICODE="$UNICODE" |