aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-user.el
diff options
context:
space:
mode:
Diffstat (limited to 'generic/pg-user.el')
-rw-r--r--generic/pg-user.el10
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))