From cd4bc763494c4e0d352878bd9f1f4d8bae60d450 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 16 Nov 1999 21:02:21 +0000 Subject: Second version of easy-config, without defvaralias use. --- generic/proof-easy-config.el | 57 +++++--------------------------------------- 1 file changed, 6 insertions(+), 51 deletions(-) (limited to 'generic/proof-easy-config.el') 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) -- cgit v1.2.3