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.

3 files changed, 17 insertions, 6 deletions

diff --git a/coq/coq.el b/coq/coq.el
index ed71b1b3..67abb4f6 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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."
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.