diff options
author | David Aspinall <da@inf.ed.ac.uk> | 1999-11-16 15:58:37 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 1999-11-16 15:58:37 +0000 |
commit | eac7e215f82098ab290a30c354969bfe3a4b27ac (patch) | |
tree | 267c41b5a9cc72c558c16ef2366b761f23909495 | |
parent | 03e7dbf10d41460ffebd871c6681df8c4eab43db (diff) |
Preliminary, not for 3.0.
-rw-r--r-- | generic/proof-easy-config.el | 99 |
1 files changed, 99 insertions, 0 deletions
diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el new file mode 100644 index 00000000..c14ca180 --- /dev/null +++ b/generic/proof-easy-config.el @@ -0,0 +1,99 @@ +;; proof-easy-config.el Easy configuration for Proof General +;; +;; Copyright (C) 1999 David Aspinall / LFCS. +;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> +;; +;; $Id$ +;; +;; Work in progress. +;; +;; XEmacs only at the moment (uses defvaralias) +;; +;; 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. +;; + +(unless (fboundp 'defvaralias) + (error "proof-easy-config only works for XEmacs, sorry!")) + + +(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)) + ("response" "resp" proof-response-mode (proof-response-config-done)) + ("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 1 modedef)) + (suffixnm (nth 2 modedef)) + (parent (nth 3 modedef)) + (body (nthcdr 4 modedef)) + (modert (concat proof-assistant-symbol "-" prefixsym)) + (modecfgfn (intern (concat modert "config"))) + (hyphen (if (string-equal prefixsym "") "" "-")) + (mode (intern (concat modert hyphen "mode"))) + (fullbody (cons (list modecfgfn) body)) + (modename (concat proof-assistant " " suffixnm)) + (varname (intern (concat "proof-mode-for-" suffixnm)))) + + `(define-derived-mode ,mode ,parent ,modename nil ,@fullbody) + + ;; A hook into the mode body, before proof-config-done is + ;; called. Probably unnecessary: the generic mode hook + ;; functions would insert code in the same place. + + `(defun ,modecfgfn () + ,(concat "Special configuration for " modert "mode. +You can redefine this function, currently it does nothing.")) + + ;; 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. + `(setq ,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) + ;; An alias which shadows ordinary proof-prog-name + (defvaralias 'proof-prog-name pn))) + +(defmacro proof-easy-config (body) + "Configure Proof General for proof-assistant using settings in BODY." + `(progn + (proof-easy-config-make-var-aliases proof-assistant-symbol 'prover-config) + (proof-easy-config-define-customs) + ,@body + (proof-easy-config-define-derived-modes))) + +;; +(provide 'proof-easy-config) + |