diff options
-rw-r--r-- | generic/pg-user.el | 10 | ||||
-rw-r--r-- | generic/proof-script.el | 11 |
2 files changed, 10 insertions, 11 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)) 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))) |