From 8416875696cb0c4283e96fe721d343277882ecea Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik@martin-dorel.org>
Date: Mon, 30 Jan 2023 11:24:17 +0100
Subject: [PATCH] feat: Make `C-c C-RET` and `C-c C-b` see prefix argument as a
 real toggle (#683)

Close ProofGeneral/PG#682
---
 doc/ProofGeneral.texi | 14 +++++++++-----
 generic/pg-user.el    | 18 +++++++++++-------
 2 files changed, 20 insertions(+), 12 deletions(-)

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 92cba3b16..49c1e6e46 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1574,16 +1574,20 @@ deleted text.
 @deffn Command proof-goto-point &optional raw
 Assert or retract to the command at current position.@*
 Calls @samp{@code{proof-assert-until-point}} or @samp{@code{proof-retract-until-point}} as
-appropriate. With prefix argument @var{raw} the omit proofs feature
-(@samp{@code{proof-omit-proofs-option}}) is temporaily disabled to check all
-proofs in the asserted region.
+appropriate.
+With prefix argument @var{raw}, the activation of the omit proofs feature
+(@samp{@code{proof-omit-proofs-option}}) is temporarily toggled,
+so we can chose whether to check all proofs in the asserted region,
+or to merely assume them and save time.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-process-buffer
 @deffn Command proof-process-buffer &optional raw
 Process the current (or script) buffer, and maybe move point to the end.@*
-With prefix argument @var{raw} the omit proofs feature (@samp{@code{proof-omit-proofs-option}})
-is temporaily disabled to check all proofs in the asserted region.
+With prefix argument @var{raw}, the activation of the omit proofs feature
+(@samp{@code{proof-omit-proofs-option}}) is temporarily toggled,
+so we can chose whether to check all proofs in the asserted region,
+or to merely assume them and save time.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-retract-buffer
diff --git a/generic/pg-user.el b/generic/pg-user.el
index c87309a45..d4115a4ba 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -168,13 +168,15 @@ If called interactively, NUM is given by the prefix argument."
 (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. With prefix argument RAW the omit proofs feature
-(`proof-omit-proofs-option') is temporaily disabled to check all
-proofs in the asserted region."
+appropriate.
+With prefix argument RAW, the activation of the omit proofs feature
+(`proof-omit-proofs-option') is temporarily toggled,
+so we can chose whether to check all proofs in the asserted region,
+or to merely assume them and save time."
   (interactive "P")
   (let ((proof-omit-proofs-option proof-omit-proofs-option))
     (when raw
-      (setq proof-omit-proofs-option nil))
+      (setq proof-omit-proofs-option (not proof-omit-proofs-option)))
     (save-excursion
       (if (> (proof-queue-or-locked-end) (point))
 	  (proof-retract-until-point)
@@ -205,12 +207,14 @@ If inside a comment, just process until the start of the comment."
 ;;;###autoload
 (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."
+With prefix argument RAW, the activation of the omit proofs feature
+(`proof-omit-proofs-option') is temporarily toggled,
+so we can chose whether to check all proofs in the asserted region,
+or to merely assume them and save time."
   (interactive "P")
   (let ((proof-omit-proofs-option proof-omit-proofs-option))
     (when raw
-      (setq proof-omit-proofs-option nil))
+      (setq proof-omit-proofs-option (not proof-omit-proofs-option)))
     (proof-with-script-buffer
      (save-excursion
        (goto-char (point-max))