Made configuration more sophisticated:

. proof-general-supported-assistants is master table of names & autoloads.
. proof-home is calculated automatically from load-file-name

1 files changed, 80 insertions, 38 deletions

diff --git a/generic/proof-site.el b/generic/proof-site.el
index 64ee3b61..9e4a89c2 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -1,16 +1,11 @@
 ;; proof-site.el --- Configuration for site and choice of prover.
 ;;
-;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
+;; Copyright (C) 1998 LFCS Edinburgh. 
 ;; Authors: David Aspinall, Thomas Kleymann
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
 ;;
 ;; $Id$
 ;;
-;; FUTURE: in the future it might be nice to allow switching between
-;; different proof assistants in the same session.  Presently, the
-;; code will only allow one assistant to be chosen for the whole
-;; session.
-;; 
 
 (or (featurep 'custom)
     ;; Quick hack to support defcustom for Emacs 19
@@ -18,29 +13,37 @@
       (defvar sym val doc))
     (defmacro group (sym mems doc &rest args)))
 
-(defgroup proof nil
+(defgroup proof-general nil
   "Customization of generic parameters for Proof General."
   :group 'external
   :group 'processes)
 
 (defcustom proof-home
-  (or (getenv "PROOF_HOME") "~/devel/lego/elisp/")
+  ;; FIXME: make sure compiling does not evaluate next expression.
+  (or (getenv "PROOF_HOME") 
+      (let ((curdir 
+	     (or
+	      (and load-in-progress (file-name-directory load-file-name))
+	      (file-name-directory (buffer-file-name)))))
+	(file-name-directory (substring curdir 0 -1))))
   "*Directory where Proof General is installed. Ends with slash.
-Default value taken from PROOF_HOME, or use customize to set it."
+Default value taken from environment variable PROOF_HOME if set, 
+otherwise based on where the file proof-site was loaded from.
+You can use customize to set this variable."
   :type 'directory
-  :group 'proof)
+  :group 'proof-general)
 
 (defcustom proof-image-directory
   (concat proof-home "images/")
     "*Where Proof General image files are installed. Ends with slash."
   :type 'directory
-  :group 'proof)
+  :group 'proof-general)
 
 (defcustom proof-info-dir 
   (concat proof-home "doc/")
   "*Where Proof General Info files are installed."
   :type 'directory
-  :group 'proof)
+  :group 'proof-general)
 
 ;; Add the info directory to the end of Emacs Info path 
 ;; if need be. 
@@ -50,47 +53,86 @@ Default value taken from PROOF_HOME, or use customize to set it."
 	   Info-default-directory-list 
 	   (list proof-info-dir))))
 
+(defconst proof-general-supported-assistants
+  '((isa	"Isabelle"	"\\.ML$\\|\\.thy$")
+    (lego	"LEGO"		"\\.l$")
+    (coq	"Coq"		"\\.v")
+    (myass	"myass"		"\\.myass"))
+  "Table of supported proof assistants.
+Each entry is a list of the form
+
+    (SYMBOL NAME AUTOLOAD-REGEXP)
+
+The NAME is a string, naming the proof assistant.
+The SYMBOL is used to form the name of the mode for the
+assistant, `SYMBOL-mode`, run when files with AUTOLOAD-REGEXP
+are loaded.  It is also used to form the name of the
+directory and elisp file for the mode, which will be
+ 
+    <proof-home>/SYMBOL/SYMBOL.el
+
+where `<proof-home>/' is the value of the variable proof-home.")
+
 (defcustom proof-assistants
-  '(isa lego coq)
-  "*Choice of proof assitants to use with Proof General.
-A list of symbol chosen from: 'lego 'coq 'isa
-NB: To change proof assistant, you must start a new Emacs session."
-  :type '(set (const :tag "Isabelle" isa)
-	      (const :tag "LEGO" lego)
-	      (const :tag "Coq" coq))
-  :group 'proof)
-
-;; Extend load path
+  (mapcar (lambda (astnt) (car astnt)) proof-general-supported-assistants)
+  (concat
+   "*Choice of proof assitants to use with Proof General.
+A list of symbols chosen from " 
+   (apply 'concat (mapcar (lambda (astnt) 
+			    (concat "'" (symbol-name (car astnt)) " "))
+			  proof-general-supported-assistants)) 
+"\nNB: To change proof assistant, you must start a new Emacs session.")
+  :type (cons 'set 
+	      (mapcar (lambda (astnt)
+			(list 'const ':tag (car (cdr astnt)) (car astnt)))
+		      proof-general-supported-assistants))
+  :group 'proof-general)
+
+;; Extend load path for the generic files.
 (setq load-path
       (cons (concat proof-home "generic/") load-path))
 
 
-;; Add auto-loads and load-path elements
-;; to support the proof assistants selected
+;; Now add auto-loads and load-path elements to support the 
+;; proof assistants selected
 (let ((assistants proof-assistants) proof-assistant)
   (while assistants
     (let*  
 	((proof-assistant (car assistants))
-	 (fileregexp 
-	  (cond ((eq proof-assistant 'coq)    "\\.v")
-		((eq proof-assistant 'lego)   "\\.l$")
-		((eq proof-assistant 'isa)    "\\.ML$\\|\\.thy$")))
-	 (assistant-name   (symbol-name proof-assistant))
-	 (proof-mode  (intern (concat assistant-name "-mode"))))
+	 (nameregexp 
+	  (or 
+	   (cdr-safe 
+	    (assoc proof-assistant proof-general-supported-assistants))
+	   (error "proof-site: symbol " (symbol-name proof-assistant) 
+		  "is not in proof-general-supported-assistants")))
+	 (assistant-name (car nameregexp))
+	 (regexp	 (car (cdr nameregexp)))
+	 (sname		 (symbol-name proof-assistant))
+	 ;; NB: File name for each prover is the same as its symbol name!
+	 (elisp-file   sname)
+	 ;; NB: Dir name for each prover is the same as its symbol name!
+	 (elisp-dir    sname)
+	 ;; NB: Mode name for each prover is <symname>-mode!
+	 (proofgen-mode  (intern (concat sname "-mode"))))
+
       (setq auto-mode-alist 
-	    (cons (cons fileregexp proof-mode) auto-mode-alist))
-      ;; NB: File name for each prover is the same as its symbol name!
-      (autoload proof-mode assistant-name
+	    (cons (cons regexp proofgen-mode) auto-mode-alist))
+      (autoload proofgen-mode elisp-file
 	(concat
-	 "Major mode for editing scripts for proof assistant " assistant-name ".")
+	 "Major mode for editing scripts for proof assistant " 
+	 assistant-name ".")
 	t)
       (setq load-path 
-	    (cons
-	     (concat proof-home (symbol-name proof-assistant) "/")
-	     load-path))
+	    (cons (concat proof-home elisp-dir "/") load-path))
       (setq assistants (cdr assistants))
+      ;; Developer's note: would be nice to add the customization group
+      ;; <sname>-settings for a particular assistant here, 
+      ;; but currently that could cause problems with more than one 
+      ;; instance of Proof General being loaded.  For the time being
+      ;; you have to visit a file before the specific prover's
+      ;; customizations appear.
       )))
-  
+
 ;; WARNING: do not edit below here 
 ;; (the next constant is set automatically)
 (defconst proof-general-version