Second version of easy-config, without defvaralias use.

1 files changed, 6 insertions, 51 deletions

diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el
index 696e6a34..81ec4f26 100644
--- a/generic/proof-easy-config.el
+++ b/generic/proof-easy-config.el
@@ -6,40 +6,12 @@
 ;;
 ;; $Id$
 ;;
-;; Work in progress.
-;; 
-;; XEmacs only at the moment (uses defvaralias)
-;;
-;; Future version might copy settings instead.  Consider how best to
+;; Future version might copy settings instead; consider how best to
 ;; interface with customization mechanism so a new prover can be
 ;; configured by editing inside custom buffers.
 ;;
-
 (require 'proof)
 
-(unless (fboundp 'defvaralias)
-  (error "proof-easy-config only works for XEmacs, sorry!"))
-
-(autoload 'custom-group-members "cus-edit")
-
-
-(defun proof-easy-config-make-var-aliases (sym group)
-  "Make variable aliases for custom GROUP, with new prefix SYM."
-  (let ((vars	  (custom-group-members group nil))
-	(prefix  (length
-		  (or (get 'custom-prefix group) ; fails sometimes, why?
-		      "proof-")))	; common prefix
-	(newpref (concat (symbol-name sym) "-")))
-    (dolist (cusmem vars)
-      (cond ((member 'custom-group cusmem)
-	     ;; recurse on subgroups
-	     (proof-easy-config-make-var-aliases sym (car cusmem)))
-	    ((member 'custom-variable cusmem)
-	     (let* ((thisone   (car cusmem))
-		    (base	(substring (symbol-name thisone) prefix))
-		    (alias	(intern (concat newpref base))))
-	       (defvaralias alias thisone)))))))
-
 (defvar proof-easy-config-derived-modes-table
   '((""         "script" proof-mode (proof-config-done))
     ("shell"    "shell"  proof-shell-mode (proof-shell-config-done))
@@ -47,9 +19,6 @@
     ("goals"	"goals"   pbp-mode (proof-goals-config-done)))
   "A list of (PREFIXSYM SUFFIXNAME PARENT MODEBODY) for derived modes.")
 
-;; FIXME: Non-uniformity in current code
-(defvaralias 'proof-mode-for-goals 'proof-mode-for-pbp)
-
 (defun proof-easy-config-define-derived-modes ()
   (dolist (modedef proof-easy-config-derived-modes-table)
     (let* ((prefixsym (nth 0 modedef))
@@ -58,30 +27,16 @@
 	   (body      (nthcdr 3 modedef))
 	   (modert    (concat (symbol-name proof-assistant-symbol)
 			      "-" prefixsym))
-	   ; config function for mode -- don't need it with global settings.
-	   ; (modecfgfn (intern (concat modert "-config")))
 	   (hyphen    (if (string-equal prefixsym "") "" "-"))
 	   (mode      (intern (concat modert hyphen "mode")))
 	   (modename  (concat proof-assistant " " suffixnm))
 	   (varname   (intern (concat "proof-mode-for-" suffixnm))))
-
       (eval
        `(define-derived-mode ,mode ,parent ,modename nil ,@body))
-
-      ;; Set proof-mode-for-script, etc.  NB: at top-level rather
-      ;; than in function body.  Then we don't need to set
-      ;; proof-pre-shell-start-hook.
+      ;; Set proof-mode-for-script and friends
+      ;; NB: top-level, so we don't need proof-pre-shell-start-hook.
       (set varname mode))))
 
-(defun proof-easy-config-define-customs ()
-  "Define a -prog-name customization setting."
-  (let* ((pn-def  (symbol-name proof-assistant-symbol))
-	 (pn	 (intern (concat pn-def "-prog-name"))))
-    `(defcustom ,pn ,pn-def
-       ,(concat "*Name of program to run " proof-assistant)
-       :type 'string
-       :group ,proof-assistant-symbol)))
-
 (defun proof-easy-config-check-setup (sym name)
   "A number of simple checks."
   (cond
@@ -102,11 +57,11 @@
   "Configure Proof General for proof-assistant using BODY as a setq body."
   `(progn
      (proof-easy-config-check-setup ,sym ,name)
-     (proof-easy-config-make-var-aliases ,sym 'prover-config)
-     (proof-easy-config-define-customs)
      (setq
       ,@body)
-     (proof-easy-config-define-derived-modes)))
+     (proof-easy-config-define-derived-modes)
+     ;; FIXME: Non-uniformity in current code
+     (setq proof-mode-for-goals proof-mode-for-pbp)))
   
 ;; 
 (provide 'proof-easy-config)