From e5cc6cf40887970e79c578ecbae00d79c288ccac Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sat, 4 May 2019 00:31:10 +0200
Subject: 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.
---
 coq/coq.el | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'coq')

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."
-- 
cgit v1.2.3