diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-user.el | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index a2be3468..bf311ebb 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -996,9 +996,11 @@ If NUM is negative, move upwards. Return new span." (defun pg-goals-buffers-hint () (pg-hint "Use \\[proof-display-some-buffers] to rotate output buffers; \\[pg-response-clear-displays] to clear response & trace.")) -(defun pg-response-buffers-hint () +(defun pg-response-buffers-hint (&optional nextbuf) (pg-hint - "Use \\[proof-prf] to refresh and display goals buffer; \\[proof-display-some-buffers] to rotate")) + (format + "Use \\[proof-prf] to display goals; \\[proof-display-some-buffers] to rotate output %s" + (if nextbuf (concat "(next: " nextbuf ")") "")))) (defun pg-processing-complete-hint () "Display hint for showing end of locked region or processing complete." |