diff options
| author | Erik Martin-Dorel | 2019-05-04 00:31:10 +0200 |
|---|---|---|
| committer | Jim Fehrle | 2019-05-16 20:33:53 -0700 |
| commit | e5cc6cf40887970e79c578ecbae00d79c288ccac (patch) | |
| tree | b62c048b73bf73bdd9ceca5b24b6f94385a0c3e2 /generic | |
| parent | 9b41ff4e90a0303d9caf6e7e2f951a5046ce2d13 (diff) | |
proof-assistant-format: Support format character "%l" a.k.a. lambda
This patch allows one to load the `coq-diffs' option at Coq startup,
provided the ambient Coq version is >= 8.10.
This additional "lambda" format is needed because [Set Diffs "on".] is neither:
- a boolean setting from Coq side (there are three possible values)
- a string setting from Emacs side (it is implemented as a radio/symbol option)
- a cross-version compatible Coq setting.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 6 | ||||
| -rw-r--r-- | generic/proof-menu.el | 8 |
2 files changed, 9 insertions, 5 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index ea7fda8f..f9947757 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -213,9 +213,9 @@ Default is the identity function." (defcustom proof-assistant-setting-format nil "Function for formatting setting strings for proof assistant. Setting strings are calculated by replacing a format character -%b, %i, or %s in the :setting string in for each variable defined with -`defpacustom', using the current value of that variable. This -function is applied as a final step to do any extra markup, or +%b, %i, %f, %s, or %l in the :setting string in for each variable +defined with `defpacustom', using the current value of that variable. +This function is applied as a final step to do any extra markup, or conversion, etc. (No changes are done if nil)." :type '(choice string (const nil)) :group 'prover-config) diff --git a/generic/proof-menu.el b/generic/proof-menu.el index ba3d05ff..c17d4e95 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -1005,7 +1005,8 @@ We first clear the dynamic settings from `proof-assistant-settings'." (cons "%b" '(proof-assistant-format-bool curvalue)) (cons "%i" '(proof-assistant-format-int curvalue)) (cons "%f" '(proof-assistant-format-float curvalue)) - (cons "%s" '(proof-assistant-format-string curvalue))) + (cons "%s" '(proof-assistant-format-string curvalue)) + (cons "%l" '(proof-assistant-format-lambda curvalue))) "Table to use with `proof-format' for formatting CURVALUE for assistant. NB: variable `curvalue' is dynamically scoped (used in `proof-assistant-format').") @@ -1021,9 +1022,12 @@ NB: variable `curvalue' is dynamically scoped (used in `proof-assistant-format') (defun proof-assistant-format-string (value) (funcall proof-assistant-format-string-fn value)) +(defun proof-assistant-format-lambda (value) + (funcall value)) + (defun proof-assistant-format (string curvalue) "Replace a format characters in STRING by formatted CURVALUE. -Format character is one of %b, %i, %f, or %s. +Format character is one of %b, %i, %f, %s, or %l. Formatting suitable for current proof assistant, controlled by `proof-assistant-format-table' which see. Finally, apply `proof-assistant-setting-format' if non-nil. |