diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-05-24 11:33:18 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-05-24 11:33:18 +0000 |
| commit | 325d4a26909c7a7a57c6ea8846da4a48c1613c73 (patch) | |
| tree | 637b461a12f4e09ad74cad6350d8c63f79461450 /generic | |
| parent | 1b92ebdd4052f001773747b94aceeaf6ffaaa1ff (diff) | |
Rotate buffers display can display next buffer
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." |