diff options
| author |  Pierre Courtieu <Matafou@users.noreply.github.com> | 2017-03-03 17:58:28 +0100 |
|---|---|---|
| committer |  Erik Martin-Dorel <erik@martin-dorel.org> | 2017-03-03 17:58:28 +0100 |
| commit | 27f06f406594632f35c6625f27875c891233511a (patch) | |
| tree | 2a11c30407d0305d2030ff08734e50fa2b2720ff /coq/coq.el | |
| parent | 12a780564aa7e5d936ebe5d9abcde5b28281f304 (diff) | |
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).
Diffstat (limited to 'coq/coq.el')
| -rw-r--r-- | coq/coq.el | 6 |
1 files changed, 4 insertions, 2 deletions
@@ -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 |