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 /coq | |
| 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 'coq')
| -rw-r--r-- | coq/coq.el | 9 |
1 files changed, 8 insertions, 1 deletions
@@ -1768,7 +1768,14 @@ See `coq-fold-hyp'." ;(proof-definvisible coq-set-printing-printing-depth "Set Printing Printing Depth . ") ;(proof-definvisible coq-unset-printing-printing-depth "Unset Printing Printing Depth . ") - +;; Persistent setting, non-boolean, non cross-version compatible (Coq >= 8.10) +(defconst coq-diffs--function #'coq-diffs + "Symbol corresponding to the function `coq-diffs'. +Required to benefit from delayed evaluation when +`proof-assistant-format-lambda' calls (funcall coq-diffs--function) +at `proof-assistant-settings-cmds' evaluation time.") +(add-to-list 'proof-assistant-settings + '(diffs--function "%l" string "Show Diffs in Coq") t) (defun coq-Compile () "Compiles current buffer." |