diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2011-01-31 12:47:43 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2011-01-31 12:47:43 +0000 |
| commit | 46b0f043d73db801a7fd340dca70d918532e4221 (patch) | |
| tree | 2447458a765b587601937a349af61488dcfcc47f | |
| parent | d52d7d723b6a48d77a8d399133f0633aed80777e (diff) | |
Only make settings commands for dynamic settings which differ from their defaults
| -rw-r--r-- | generic/pg-pamacs.el | 6 | ||||
| -rw-r--r-- | generic/proof-menu.el | 21 |
2 files changed, 19 insertions, 8 deletions
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el index c8bac3a5..de05c04d 100644 --- a/generic/pg-pamacs.el +++ b/generic/pg-pamacs.el @@ -65,6 +65,12 @@ This macro should only be invoked once a specific prover is engaged." `(symbol-value (intern (concat (symbol-name proof-assistant-symbol) "-" (symbol-name ',sym))))) +(defun proof-ass-differs-from-default (sym) + "Return non-nil if SYM for current prover differs from its customize standard value." + (let ((pasym (proof-ass-symv sym))) + (not (equal (eval (car (get pasym 'standard-value))) + (symbol-value pasym))))) + (defun proof-defpgcustom-fn (sym args) "Define a new customization variable <PA>-sym for current proof assistant. Helper for macro `defpgcustom'." diff --git a/generic/proof-menu.el b/generic/proof-menu.el index cc4e850e..798dba89 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -937,7 +937,7 @@ We first clear the dynamic settings from `proof-assistant-settings'." (defun proof-assistant-settings-cmd (setting) "Return string for making SETTING in Proof General customization." - (let ((expr (assoc setting proof-assistant-settings))) + (let ((expr (assq setting proof-assistant-settings))) (if (and expr (cadr expr)) (proof-assistant-format (cadr expr) @@ -945,13 +945,18 @@ We first clear the dynamic settings from `proof-assistant-settings'." (defun proof-assistant-settings-cmds () "Return strings for settings kept in Proof General customizations." - (when proof-assistant-settings - (mapcar (lambda (expr) - (if (cadr expr) ;; setting has PA string? - (proof-assistant-format - (cadr expr) - (eval (proof-ass-symv (car expr)))))) - proof-assistant-settings))) + (let (cmds) + (dolist (setting proof-assistant-settings) + (let ((sym (car setting)) + (pacmd (cadr setting))) + (if (and pacmd + (or (not (get sym 'pgdynamic)) + (proof-ass-differs-from-default sym))) + (push (proof-assistant-format pacmd + (eval (proof-ass-symv sym))) + cmds)))) + cmds)) + (defvar proof-assistant-format-table (list |