From 91c7cb718f35c0fb4485cd6afe9c9529cd38d603 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Thu, 7 Dec 2006 19:51:41 +0000
Subject: removed obsolete references to 'isa';

---
 Makefile              |  4 ++--
 generic/proof-site.el |  4 ----
 isar/interface        | 24 +++++-------------------
 isar/x-symbol-isar.el |  2 +-
 4 files changed, 8 insertions(+), 26 deletions(-)

diff --git a/Makefile b/Makefile
index d7f32c78..6ed3f61a 100644
--- a/Makefile
+++ b/Makefile
@@ -28,14 +28,14 @@ DEST_PREFIX=/usr
 
 PWD=$(shell pwd)
 
-PROVERS=acl2 ccc coq demoisa hol98 isa isar lclam lego pgshell phox plastic twelf
+PROVERS=acl2 ccc coq demoisa hol98 isar lclam lego pgshell phox plastic twelf
 OTHER_ELISP=generic lib mmm
 ELISP_DIRS=${PROVERS} ${OTHER_ELISP}
 ELISP_EXTRAS=isar/interface isar/isartags
 EXTRA_DIRS = images x-symbol
 
 DOC_FILES=AUTHORS BUGS CHANGES COPYING INSTALL README.* REGISTER doc/*.pdf
-DOC_EXAMPLES=acl2/*.acl2 hol98/*.sml isa/*.ML isa/*.thy isar/*.thy lclam/*.lcm lego/*.l pgshell/*.pgsh phox/*.phx plastic/*.lf twelf/*.elf
+DOC_EXAMPLES=acl2/*.acl2 hol98/*.sml isar/*.thy lclam/*.lcm lego/*.l pgshell/*.pgsh phox/*.phx plastic/*.lf twelf/*.elf
 DOC_SUBDIRS=${DOC_EXAMPLES} */README.* */CHANGES */BUGS 
 
 BATCHEMACS=${EMACS} -batch -q -no-site-file
diff --git a/generic/proof-site.el b/generic/proof-site.el
index c26024e5..579e074e 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -106,9 +106,6 @@ You can use customize to set this variable."
 	    (list dne)
 	  nil)))
    '(
-;; To use classic Isabelle instead of Isabelle/Isar,
-;; uncomment appropriate line below and set
-;; export PROOFGENERAL_ASSISTANTS=isar
 ;;
 ;; To Use HOL, uncomment the line below.  It's disabled
 ;; by default because of clash with SML mode (same for .ML).
@@ -118,7 +115,6 @@ You can use customize to set this variable."
 ;; export PROOFGENERAL_ASSISTANTS=demoisa. 
 ;;
 ;;    (demoisa    "Isabelle Demo"	"\\.ML$")
-;;    (isa        "Isabelle"	"\\.ML$\\|\\.thy$")
     (isar       "Isabelle"      "\\.thy$")
     (lego	"LEGO"		"\\.l$")
     (coq	"Coq"		"\\.v$\\|\\.v8$\\|\\.v7$")
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
-- 
cgit v1.2.3