Fix pg-{show,hide}-all-proofs and Move them into pg-user.el.

This commit address ProofGeneral/PG#193.

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)))