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 /generic/pg-pamacs.el | |
| parent | d52d7d723b6a48d77a8d399133f0633aed80777e (diff) | |
Only make settings commands for dynamic settings which differ from their defaults
Diffstat (limited to 'generic/pg-pamacs.el')
| -rw-r--r-- | generic/pg-pamacs.el | 6 |
1 files changed, 6 insertions, 0 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'." |