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 | |
| parent | a4b24e4e30d10a79f3d8fc90d1acd69b80b4c2ab (diff) | |
removed obsolete references to 'isa';
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/interface | 24 | ||||
| -rw-r--r-- | isar/x-symbol-isar.el | 2 |
2 files changed, 6 insertions, 20 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" diff --git a/isar/x-symbol-isar.el b/isar/x-symbol-isar.el index 684a2a21..9fb90930 100644 --- a/isar/x-symbol-isar.el +++ b/isar/x-symbol-isar.el @@ -7,7 +7,7 @@ ;; x-symbol support ;; ;; The following settings configure the generic PG package. -;; The token language "Isabelle Symbols" is in file isa/x-symbol-isabelle.el +;; The token language "Isabelle Symbols" is in file isar/x-symbol-isabelle.el ;; (setq |