From 2e22e81302a81fd5c1583a6edad179551805dc29 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 6 Jun 2017 15:35:51 +0200 Subject: Adding a Set Silent + Show when backtracking into a proof. Checking whether the backtrack is inside a proof or not is a bit convoluted but seems ok. --- coq/coq.el | 32 +++++++++++++++++++++++--------- 1 file changed, 23 insertions(+), 9 deletions(-) (limited to 'coq/coq.el') diff --git a/coq/coq.el b/coq/coq.el index d8a52983..5a24dbb1 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1231,15 +1231,29 @@ flag Printing All set." the last command of the action list. If CMD is tagged with 'empty-action-list then this function won't be called and no command will be sent to coq. " - (when (or - ;; If clsing a nested proof, return t. - (and (string-match coq-save-command-regexp-strict cmd) - (> (length coq-last-but-one-proofstack) 1)) - ;; If user issued a printing option then t printing. - (and (string-match "\\(S\\|Uns\\)et\\s-+Printing" cmd) - (> (length coq-last-but-one-proofstack) 0))) - (list "Show."))) - + (cond + ((or + ;; If closing a nested proof, Show the enclosing goal. + (and (string-match coq-save-command-regexp-strict cmd) + (> (length coq-last-but-one-proofstack) 1)) + ;; If user issued a printing option then t printing. + (and (string-match "\\(S\\|Uns\\)et\\s-+Printing" cmd) + (> (length coq-last-but-one-proofstack) 0))) + (list "Show.")) + ((or + ;; if we go back in the buffer and that the number of abort is less than + ;; the number of nested goals, then Unset Silent and Show the goal + (and (string-match "Backtrack\\s-+[[:digit:]]+\\s-+[[:digit:]]+\\(\\s-+[[:digit:]]*\\)" cmd) + (> (length (coq-get-span-proofstack (proof-last-locked-span))) + ;; the number of aborts is the third arg of Backtrack. + (string-to-number (match-string 1 cmd))))) + (list "Unset Silent." "Show.")) + ((or + ;; If we go back in the buffer and not in the above case, then only Unset + ;; silent (there is no goal to show). + (string-match "Backtrack" cmd)) + (list "Unset Silent.")))) + (defpacustom auto-adapt-printing-width t "If non-nil, adapt automatically printing width of goals window. Each timme the user sends abunch of commands to Coq, check if the -- cgit v1.2.3