From 9083698d0bbd4438208fa72222438ae59684542d Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 15 Aug 2017 11:31:36 +0200 Subject: Fix pg-{show,hide}-all-proofs and Move them into pg-user.el. This commit address ProofGeneral/PG#193. --- generic/pg-user.el | 10 ++++++++++ generic/proof-script.el | 11 ----------- 2 files changed, 10 insertions(+), 11 deletions(-) (limited to 'generic') 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)) diff --git a/generic/proof-script.el b/generic/proof-script.el index 7d9afe22..eb8fac7a 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -633,17 +633,6 @@ IDIOMSYM is a symbol and ID is a strings." (proof-with-script-buffer ; may be called from menu (maphash alterfn elts))))) -;; Next two could be in pg-user.el. No key-bindings for these. -(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)) - (defun pg-add-proof-element (name span controlspan) "Add a span proof element to SPAN with name NAME and parent CONTROLSPAN." (let ((proofid (proof-next-element-id 'proof))) -- cgit v1.2.3