diff options
| author |  Erik Martin-Dorel <erik@martin-dorel.org> | 2017-08-15 11:31:36 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel <erik@martin-dorel.org> | 2017-08-15 11:31:36 +0200 |
| commit | 9083698d0bbd4438208fa72222438ae59684542d (patch) | |
| tree | 2d35fa4c7c3668fddb97334b6474c473706a03b7 /generic/pg-user.el | |
| parent | e4b4155b3813f0eedf808ece4b0aef86c8abc1c0 (diff) | |
Fix pg-{show,hide}-all-proofs and Move them into pg-user.el.
This commit address ProofGeneral/PG#193.
Diffstat (limited to 'generic/pg-user.el')
| -rw-r--r-- | generic/pg-user.el | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index effe1eb5..11a731fb 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -702,6 +702,16 @@ If NUM is negative, move upwards. Return new span." (interactive "p") (pg-move-region-down (- num))) +;; No key-binding is defined for these two functions: +(defun pg-show-all-proofs () + "Display all completed proofs in the buffer." + (interactive) + (pg-show-all-portions 'proof)) + +(defun pg-hide-all-proofs () + "Hide all completed proofs in the buffer." + (interactive) + (pg-show-all-portions 'proof 'hide)) |