From 0c4d7e6e96bfc798a2663de2d2a21c654b756175 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 18 Nov 2002 23:08:45 +0000 Subject: Support redefinitions in proof-defpacustom-fn, by removing custom settings. --- generic/proof-menu.el | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) (limited to 'generic/proof-menu.el') diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 6161f72a..f7dec051 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -586,7 +586,7 @@ the form of the menu entry for the setting.") ;;; autoload for compiled version: used in macro proof-defpacustom ;;;###autoload (defun proof-defpacustom-fn (name val args) - "As for macro `defpacustom' but evaluation arguments." + "As for macro `defpacustom' but evaluating arguments." (let (newargs setting evalform type) (while args (cond @@ -614,15 +614,19 @@ the form of the menu entry for the setting.") ;; NB: this *may* happen dynamically, but shouldn't: if the ;; interface queries the prover for the settings it supports, ;; then the internal list should be cleared first. + ;; FIXME: for now, we support redefinitions, by calling + ;; pg-custom-undeclare-variable. (if (assoc name proof-assistant-settings) - (proof-debug "defpacustom: Proof assistanting setting %s re-defined!" - name)) + (progn + (proof-debug "defpacustom: Proof assistanting setting %s re-defined!" + name) + (undefpgcustom name))) ;; Could consider moving the bulk of the remainder of this ;; function to a function proof-assistant-setup-settings which - ;; defines the custom vals *and* menu entries. This would - ;; allow proof assistant customization to manipulate - ;; proof-assistant-settings directly rather than forcing - ;; use of defpacustom. (Probably stay as we are: more abstract) + ;; defines the custom vals *and* menu entries. This would allow + ;; proof assistant customization to manipulate + ;; proof-assistant-settings directly rather than forcing use of + ;; defpacustom. (Probably stay as we are: more abstract) (eval `(defpgcustom ,name ,val ,@newargs @@ -721,7 +725,9 @@ NB: variable curvalue is dynamically scoped (used in proof-assistant-format).") (defun proof-assistant-format-string (value) (funcall proof-assistant-format-string-fn value)) - + + + (provide 'proof-menu) -- cgit v1.2.3