prefix arg for temporarily disabling omitting proofs

Make proof-goto-point and proof-process-buffer prefix argument
aware. With argument, both commands temporarily switch off
proof-omit-proofs-option, such that all proofs are completely
processed for one particular invocation.

2 files changed, 38 insertions, 24 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index f10f02c1..005d919e 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -165,19 +165,24 @@ If called interactively, NUM is given by the prefix argument."
 ;;
 
 ;;;###autoload
-(defun proof-goto-point ()
+(defun proof-goto-point (&optional raw)
   "Assert or retract to the command at current position.
 Calls `proof-assert-until-point' or `proof-retract-until-point' as
-appropriate."
-  (interactive)
-  (save-excursion
-    (if (> (proof-queue-or-locked-end) (point))
-	(proof-retract-until-point)
-      (if (proof-only-whitespace-to-locked-region-p)
-	  (progn
-	    (skip-chars-forward " \t\n")
-	    (forward-char 1)))
-      (proof-assert-until-point))))
+appropriate. With prefix argument RAW the omit proofs feature
+(`proof-omit-proofs-option') is temporaily disabled to check all
+proofs in the asserted region."
+  (interactive "P")
+  (let ((proof-omit-proofs-option proof-omit-proofs-option))
+    (when raw
+      (setq proof-omit-proofs-option nil))
+    (save-excursion
+      (if (> (proof-queue-or-locked-end) (point))
+	  (proof-retract-until-point)
+        (if (proof-only-whitespace-to-locked-region-p)
+	    (progn
+	      (skip-chars-forward " \t\n")
+	      (forward-char 1)))
+        (proof-assert-until-point)))))
 
 (defun proof-assert-next-command-interactive ()
   "Process until the end of the next unprocessed command after point.
@@ -198,18 +203,23 @@ If inside a comment, just process until the start of the comment."
   (proof-assert-until-point))
 
 ;;;###autoload
-(defun proof-process-buffer ()
-  "Process the current (or script) buffer, and maybe move point to the end."
-  (interactive)
-  (proof-with-script-buffer
-   (save-excursion
-     (goto-char (point-max))
-     (proof-assert-until-point-interactive))
-   (proof-maybe-follow-locked-end))
-  (when proof-fast-process-buffer
-    (message "Processing buffer...")
-    (proof-shell-wait)
-    (message "Processing buffer...done")))
+(defun proof-process-buffer (&optional raw)
+  "Process the current (or script) buffer, and maybe move point to the end.
+With prefix argument RAW the omit proofs feature (`proof-omit-proofs-option')
+is temporaily disabled to check all proofs in the asserted region."
+  (interactive "P")
+  (let ((proof-omit-proofs-option proof-omit-proofs-option))
+    (when raw
+      (setq proof-omit-proofs-option nil))
+    (proof-with-script-buffer
+     (save-excursion
+       (goto-char (point-max))
+       (proof-assert-until-point-interactive))
+     (proof-maybe-follow-locked-end))
+    (when proof-fast-process-buffer
+      (message "Processing buffer...")
+      (proof-shell-wait)
+      (message "Processing buffer...done"))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index d5df0404..1432776f 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -106,7 +106,11 @@ sent to the proof assistant (and thus not checked). For files
 with big proofs this can drastically reduce the processing time
 for the asserted region at the cost of not checking the proofs.
 For partial and non-opaque proofs in the asserted region all
-proof commands are sent to the proof assistant."
+proof commands are sent to the proof assistant.
+
+Using a prefix argument for `proof-goto-point' (\\[proof-goto-point])
+or `proof-process-buffer' (\\[proof-process-buffer]) temporarily
+disables omitting proofs."
   :type 'boolean
   :group 'proof-user-options)