From 27f06f406594632f35c6625f27875c891233511a Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 3 Mar 2017 17:58:28 +0100 Subject: Refreshing goal when Set Printing xxx. (#162) * Close ProofGeneral/PG#161. Issue a "Show" each time a (Uns|S)et Printing is detected (and a proof is open). --- coq/coq.el | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'coq/coq.el') diff --git a/coq/coq.el b/coq/coq.el index bd274413..d0fe0778 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1224,8 +1224,10 @@ flag Printing All set." ;; inserts a "Show" if the last command of an action list is a save command and ;; there is more than one open proof before that save. (defun coq-empty-action-list-command (cmd) - (when (and (string-match coq-save-command-regexp-strict cmd) - (> (length coq-last-but-one-proofstack) 1)) + (when (or (and (string-match coq-save-command-regexp-strict cmd) + (> (length coq-last-but-one-proofstack) 1)) + (and (string-match "\\(S\\|Uns\\)et\\s-+Printing" cmd) + (> (length coq-last-but-one-proofstack) 0))) (list "Show."))) (defpacustom auto-adapt-printing-width t -- cgit v1.2.3