From 8e12eee54e36ca16d4b4530e1509479f22929e4f Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Mon, 11 May 2020 15:00:47 +0200
Subject: First try for feature #487

---
 coq/coq-abbrev.el         |  9 +++++++--
 coq/coq-compile-common.el | 10 ++++++++++
 coq/coq-showdiff.el       | 12 ++++++++++++
 coq/coq.el                |  9 ++++++++-
 4 files changed, 37 insertions(+), 3 deletions(-)
 create mode 100644 coq/coq-showdiff.el

(limited to 'coq')

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index bd898a9c..4d2c8287 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -78,7 +78,7 @@
 ;; Common part (script, response and goals buffers)
 (defconst coq-menu-common-entries
   `(
-    ["Toggle 3 Windows Mode" proof-three-window-toggle
+      ["Toggle 3 Windows Mode" proof-three-window-toggle
      :style toggle
      :selected proof-three-window-enable
      :help "Toggles the use of separate windows or frames for Coq responses and goals."
@@ -243,7 +243,7 @@
       :active (and coq-compile-before-require
 		   coq-compile-parallel-in-background)
       :help "Abort background compilation and kill all compilation processes."])
-    ("Diffs"
+     ("Diffs"
       ["off"
        (customize-set-variable 'coq-diffs 'off)
        :style radio
@@ -259,6 +259,11 @@
        :style radio
        :selected (eq coq-diffs 'removed)
        :help "Show diffs: added and removed"])
+    ["Show proof diffs"
+      coq-show-proof-toggle
+      :style toggle
+      :selected coq-show-proof
+      :help "Show the proof diffs in the response buffer"]
     ("\"Proof using\" mode..."
      ["ask"
       (customize-set-variable 'coq-accept-proof-using-suggestion 'ask)
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index f9a3571e..2a5c3f44 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -458,6 +458,16 @@ This option can be set via menu
 ;; define coq-lock-ancestors-toggle
 (proof-deftoggle coq-lock-ancestors)
 
+;; Maybe not the good place
+(defcustom coq-show-proof nil
+  "TODO: doc"
+
+  :type 'boolean
+  :safe 'booleanp
+  :group 'coq-auto-compile)
+
+(proof-deftoggle coq-show-proof)
+
 (defcustom coq-confirm-external-compilation t
   "If set let user change and confirm the compilation command.
 Otherwise start the external compilation without confirmation.
diff --git a/coq/coq-showdiff.el b/coq/coq-showdiff.el
new file mode 100644
index 00000000..f42431af
--- /dev/null
+++ b/coq/coq-showdiff.el
@@ -0,0 +1,12 @@
+;; Temporary file, just for test
+(defun coq-show-proof-fun ()
+  (interactive)
+  ;; TODO: Check if we are in a proof
+  (when coq-show-proof
+    (when (eq coq-diffs 'off)
+      (proof-shell-invisible-command "Show Proof." ))
+    (when (eq coq-diffs 'on)
+      (proof-shell-invisible-command "Show Proof Diffs."))
+    (when (eq coq-diffs 'removed)
+      (proof-shell-invisible-command "Show Proof Diffs removed.")))
+ )
\ No newline at end of file
diff --git a/coq/coq.el b/coq/coq.el
index 71112fc1..8ebf3054 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1222,7 +1222,14 @@ be called and no command will be sent to Coq."
      (string-match-p "BackTo\\s-" cmd))
     (if (coq--post-v810)
         (list "Unset Silent." (coq-diffs))
-      (list "Unset Silent.")))))
+      (list "Unset Silent.")))
+   ((or
+     ;; If doing (not closing) a proof, Show Proof if need be
+     (and (not (string-match-p coq-save-command-regexp-strict cmd))
+          (> (length coq-last-but-one-proofstack) 0)
+          (when coq-show-proof
+            (list  "Show Proof." "Show.")))))))
+
 
 (defpacustom auto-adapt-printing-width t
   "If non-nil, adapt automatically printing width of goals window.
-- 
cgit v1.2.3


From ecb47478c9f9959ea25ce509076f6e3959d2c620 Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Thu, 14 May 2020 15:29:58 +0200
Subject: All case for Show and regex variable

---
 coq/coq-syntax.el |  3 +++
 coq/coq.el        | 21 ++++++++++++++++++---
 2 files changed, 21 insertions(+), 3 deletions(-)

(limited to 'coq')

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 470331a6..e486997d 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1304,6 +1304,9 @@ It is used:
   "*Font-lock table for Coq terms.")
 
 
+(defconst coq-show-diffs-regexp
+  "Show Proof\\(\\.\\| Diffs\\.\\| Diffs removed\\.\\)")
+
 (defconst coq-save-command-regexp
   ;; FIXME: The surrounding grouping parens are probably not needed.
   (concat "\\`\\(\\(?:Time\\s-+\\|Timeout\\s-+[[:digit:]]+\\s-+\\)*\\_<"
diff --git a/coq/coq.el b/coq/coq.el
index 8ebf3054..65ff488f 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1208,14 +1208,27 @@ be called and no command will be sent to Coq."
      ;; If user issued a printing option then t printing.
      (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd)
           (> (length coq-last-but-one-proofstack) 0)))
-    (list "Show."))
+    (if coq-show-proof
+        (or
+    (when (eq coq-diffs 'off) (list "Show." "Show Proof." ))
+    (when (eq coq-diffs 'on) (list "Show." "Show Proof Diffs."))
+    (when (eq coq-diffs 'removed) (list "Show." "Show Proof Diffs removed.")))
+   (list "Show.")))
    ((or
      ;; If we go back in the buffer and the number of abort is less than
      ;; the number of nested goals, then Unset Silent and Show the goal
      (and (string-match-p "BackTo\\s-" cmd)
           (> (length coq-last-but-one-proofstack) coq--retract-naborts)))
     ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs
-    (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")))
+    (list "Unset Silent." (if (coq--post-v810) (coq-diffs)
+                            (if coq-show-proof
+    ((when (eq coq-diffs 'off)
+      "Show." "Show Proof." )
+    (when (eq coq-diffs 'on)
+      "Show." "Show Proof Diffs.")
+    (when (eq coq-diffs 'removed)
+       "Show." "Show Proof Diffs removed."))
+     "Show."))))
    ((or
      ;; If we go back in the buffer and not in the above case, then only Unset
      ;; silent (there is no goal to show). Still, we need to "Set Diffs" again
@@ -1228,7 +1241,7 @@ be called and no command will be sent to Coq."
      (and (not (string-match-p coq-save-command-regexp-strict cmd))
           (> (length coq-last-but-one-proofstack) 0)
           (when coq-show-proof
-            (list  "Show Proof." "Show.")))))))
+            (list "Show." "Show Proof.")))))))
 
 
 (defpacustom auto-adapt-printing-width t
@@ -1897,6 +1910,8 @@ at `proof-assistant-settings-cmds' evaluation time.")
         proof-save-command "Save %s. "
         proof-find-theorems-command "Search %s. ")
 
+  (setq proof-show-diffs-regexp coq-show-diffs-regexp)
+
   (setq proof-shell-empty-action-list-command 'coq-empty-action-list-command)
 
 ;; FIXME da: Does Coq have a help or about command?
-- 
cgit v1.2.3


From aba3f2bfe2bffde6d2df21b098740100459a84be Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 15 May 2020 15:50:48 +0200
Subject: Fix name clash & rephrase some strings

---
 coq/coq-abbrev.el         | 8 ++++----
 coq/coq-compile-common.el | 4 ++--
 coq/coq-showdiff.el       | 4 ++--
 coq/coq-syntax.el         | 3 ++-
 coq/coq.el                | 8 ++++----
 5 files changed, 14 insertions(+), 13 deletions(-)

(limited to 'coq')

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 4d2c8287..74ddb076 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -259,11 +259,11 @@
        :style radio
        :selected (eq coq-diffs 'removed)
        :help "Show diffs: added and removed"])
-    ["Show proof diffs"
-      coq-show-proof-toggle
+    ["Show Proof (Diffs)"
+      coq-show-proof-stepwise-toggle
       :style toggle
-      :selected coq-show-proof
-      :help "Show the proof diffs in the response buffer"]
+      :selected coq-show-proof-stepwise
+      :help "Display the proof terms stepwise in the *response* buffer."]
     ("\"Proof using\" mode..."
      ["ask"
       (customize-set-variable 'coq-accept-proof-using-suggestion 'ask)
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 2a5c3f44..fdb3d4b8 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -459,14 +459,14 @@ This option can be set via menu
 (proof-deftoggle coq-lock-ancestors)
 
 ;; Maybe not the good place
-(defcustom coq-show-proof nil
+(defcustom coq-show-proof-stepwise nil
   "TODO: doc"
 
   :type 'boolean
   :safe 'booleanp
   :group 'coq-auto-compile)
 
-(proof-deftoggle coq-show-proof)
+(proof-deftoggle coq-show-proof-stepwise)
 
 (defcustom coq-confirm-external-compilation t
   "If set let user change and confirm the compilation command.
diff --git a/coq/coq-showdiff.el b/coq/coq-showdiff.el
index f42431af..0daf98f8 100644
--- a/coq/coq-showdiff.el
+++ b/coq/coq-showdiff.el
@@ -2,11 +2,11 @@
 (defun coq-show-proof-fun ()
   (interactive)
   ;; TODO: Check if we are in a proof
-  (when coq-show-proof
+  (when coq-show-proof-stepwise
     (when (eq coq-diffs 'off)
       (proof-shell-invisible-command "Show Proof." ))
     (when (eq coq-diffs 'on)
       (proof-shell-invisible-command "Show Proof Diffs."))
     (when (eq coq-diffs 'removed)
       (proof-shell-invisible-command "Show Proof Diffs removed.")))
- )
\ No newline at end of file
+ )
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index e486997d..a27274c5 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1304,7 +1304,8 @@ It is used:
   "*Font-lock table for Coq terms.")
 
 
-(defconst coq-show-diffs-regexp
+(defconst coq-show-proof-diffs-regexp
+  ;; FIXME/TODO: enhance this regexp
   "Show Proof\\(\\.\\| Diffs\\.\\| Diffs removed\\.\\)")
 
 (defconst coq-save-command-regexp
diff --git a/coq/coq.el b/coq/coq.el
index 65ff488f..b833765f 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1208,7 +1208,7 @@ be called and no command will be sent to Coq."
      ;; If user issued a printing option then t printing.
      (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd)
           (> (length coq-last-but-one-proofstack) 0)))
-    (if coq-show-proof
+    (if coq-show-proof-stepwise
         (or
     (when (eq coq-diffs 'off) (list "Show." "Show Proof." ))
     (when (eq coq-diffs 'on) (list "Show." "Show Proof Diffs."))
@@ -1221,7 +1221,7 @@ be called and no command will be sent to Coq."
           (> (length coq-last-but-one-proofstack) coq--retract-naborts)))
     ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs
     (list "Unset Silent." (if (coq--post-v810) (coq-diffs)
-                            (if coq-show-proof
+                            (if coq-show-proof-stepwise
     ((when (eq coq-diffs 'off)
       "Show." "Show Proof." )
     (when (eq coq-diffs 'on)
@@ -1240,7 +1240,7 @@ be called and no command will be sent to Coq."
      ;; If doing (not closing) a proof, Show Proof if need be
      (and (not (string-match-p coq-save-command-regexp-strict cmd))
           (> (length coq-last-but-one-proofstack) 0)
-          (when coq-show-proof
+          (when coq-show-proof-stepwise
             (list "Show." "Show Proof.")))))))
 
 
@@ -1910,7 +1910,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
         proof-save-command "Save %s. "
         proof-find-theorems-command "Search %s. ")
 
-  (setq proof-show-diffs-regexp coq-show-diffs-regexp)
+  (setq proof-show-proof-diffs-regexp coq-show-proof-diffs-regexp)
 
   (setq proof-shell-empty-action-list-command 'coq-empty-action-list-command)
 
-- 
cgit v1.2.3


From 04aff704f3d13452bc5c52ff860c5ab564539632 Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Mon, 18 May 2020 13:33:57 +0200
Subject: WIP for #487

---
 coq/coq-syntax.el | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'coq')

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index a27274c5..3ae7fbca 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1305,8 +1305,7 @@ It is used:
 
 
 (defconst coq-show-proof-diffs-regexp
-  ;; FIXME/TODO: enhance this regexp
-  "Show Proof\\(\\.\\| Diffs\\.\\| Diffs removed\\.\\)")
+  "^[ ]*Show Proof\\( Diffs\\| Diffs removed\\)?\\.$")
 
 (defconst coq-save-command-regexp
   ;; FIXME: The surrounding grouping parens are probably not needed.
-- 
cgit v1.2.3


From 22681a3caf2c8f45700585ea74dffbf48bb2ac19 Mon Sep 17 00:00:00 2001
From: Cyril Anaclet
Date: Wed, 20 May 2020 14:19:14 +0200
Subject: Apply reviews of @erikmd

---
 coq/coq-compile-common.el |  8 --------
 coq/coq-showdiff.el       | 12 ------------
 coq/coq-syntax.el         |  2 +-
 coq/coq.el                | 44 ++++++++++++++++++++++++++++----------------
 4 files changed, 29 insertions(+), 37 deletions(-)
 delete mode 100644 coq/coq-showdiff.el

(limited to 'coq')

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index fdb3d4b8..938f706e 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -458,14 +458,6 @@ This option can be set via menu
 ;; define coq-lock-ancestors-toggle
 (proof-deftoggle coq-lock-ancestors)
 
-;; Maybe not the good place
-(defcustom coq-show-proof-stepwise nil
-  "TODO: doc"
-
-  :type 'boolean
-  :safe 'booleanp
-  :group 'coq-auto-compile)
-
 (proof-deftoggle coq-show-proof-stepwise)
 
 (defcustom coq-confirm-external-compilation t
diff --git a/coq/coq-showdiff.el b/coq/coq-showdiff.el
deleted file mode 100644
index 0daf98f8..00000000
--- a/coq/coq-showdiff.el
+++ /dev/null
@@ -1,12 +0,0 @@
-;; Temporary file, just for test
-(defun coq-show-proof-fun ()
-  (interactive)
-  ;; TODO: Check if we are in a proof
-  (when coq-show-proof-stepwise
-    (when (eq coq-diffs 'off)
-      (proof-shell-invisible-command "Show Proof." ))
-    (when (eq coq-diffs 'on)
-      (proof-shell-invisible-command "Show Proof Diffs."))
-    (when (eq coq-diffs 'removed)
-      (proof-shell-invisible-command "Show Proof Diffs removed.")))
- )
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 3ae7fbca..47869aed 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1305,7 +1305,7 @@ It is used:
 
 
 (defconst coq-show-proof-diffs-regexp
-  "^[ ]*Show Proof\\( Diffs\\| Diffs removed\\)?\\.$")
+  "\\bShow Proof\\(?: Diffs\\| Diffs removed\\)?\\.\\b")
 
 (defconst coq-save-command-regexp
   ;; FIXME: The surrounding grouping parens are probably not needed.
diff --git a/coq/coq.el b/coq/coq.el
index b833765f..942e85fe 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -160,6 +160,16 @@ See also option `coq-hide-additional-subgoals'."
   :type '(choice regexp (const nil))
   :group 'coq)
 
+(defcustom coq-show-proof-stepwise nil
+  "Display the proof terms stepwise in the *response* buffer.
+  This option can be combined with option `coq-diffs'.
+  It is mostly useful in three window mode, see also
+  `proof-three-window-mode-policy' for details."
+
+  :type 'boolean
+  :safe 'booleanp
+  :group 'coq-auto-compile)
+
 ;;
 ;; prooftree customization
 ;;
@@ -1208,40 +1218,42 @@ be called and no command will be sent to Coq."
      ;; If user issued a printing option then t printing.
      (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd)
           (> (length coq-last-but-one-proofstack) 0)))
-    (if coq-show-proof-stepwise
+    (list "Show."
+    (when coq-show-proof-stepwise
         (or
-    (when (eq coq-diffs 'off) (list "Show." "Show Proof." ))
-    (when (eq coq-diffs 'on) (list "Show." "Show Proof Diffs."))
-    (when (eq coq-diffs 'removed) (list "Show." "Show Proof Diffs removed.")))
-   (list "Show.")))
+    (when (eq coq-diffs 'off) "Show Proof.")
+    (when (eq coq-diffs 'on) "Show Proof Diffs.")
+    (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
+   
    ((or
      ;; If we go back in the buffer and the number of abort is less than
      ;; the number of nested goals, then Unset Silent and Show the goal
      (and (string-match-p "BackTo\\s-" cmd)
           (> (length coq-last-but-one-proofstack) coq--retract-naborts)))
     ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs
-    (list "Unset Silent." (if (coq--post-v810) (coq-diffs)
-                            (if coq-show-proof-stepwise
-    ((when (eq coq-diffs 'off)
-      "Show." "Show Proof." )
-    (when (eq coq-diffs 'on)
-      "Show." "Show Proof Diffs.")
-    (when (eq coq-diffs 'removed)
-       "Show." "Show Proof Diffs removed."))
-     "Show."))))
+    (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")
+                                  (when coq-show-proof-stepwise
+                                    (or
+    (when (eq coq-diffs 'off) "Show Proof.")
+    (when (eq coq-diffs 'on) "Show Proof Diffs.")
+    (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
+
    ((or
      ;; If we go back in the buffer and not in the above case, then only Unset
      ;; silent (there is no goal to show). Still, we need to "Set Diffs" again
      (string-match-p "BackTo\\s-" cmd))
     (if (coq--post-v810)
-        (list "Unset Silent." (coq-diffs))
+        (list "Unset Silent." (coq-diffs) )
       (list "Unset Silent.")))
    ((or
      ;; If doing (not closing) a proof, Show Proof if need be
      (and (not (string-match-p coq-save-command-regexp-strict cmd))
           (> (length coq-last-but-one-proofstack) 0)
           (when coq-show-proof-stepwise
-            (list "Show." "Show Proof.")))))))
+              (or
+    (when (eq coq-diffs 'off) (list "Show Proof." ))
+    (when (eq coq-diffs 'on) (list "Show Proof Diffs."))
+    (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))))))))
 
 
 (defpacustom auto-adapt-printing-width t
-- 
cgit v1.2.3


From 411ebb27fda4d39fc22baf341dcdde2341632b8d Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 20 May 2020 21:48:20 +0200
Subject: fix: Do "Show Proof…" (with "?Goal") as soon as the proof is started

---
 coq/coq.el | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 942e85fe..10aa07bf 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1246,14 +1246,16 @@ be called and no command will be sent to Coq."
         (list "Unset Silent." (coq-diffs) )
       (list "Unset Silent.")))
    ((or
+     ;; If starting a proof, Show Proof if need be
+     (coq-goal-command-str-p cmd)
      ;; If doing (not closing) a proof, Show Proof if need be
      (and (not (string-match-p coq-save-command-regexp-strict cmd))
-          (> (length coq-last-but-one-proofstack) 0)
+          (> (length coq-last-but-one-proofstack) 0)))
           (when coq-show-proof-stepwise
               (or
     (when (eq coq-diffs 'off) (list "Show Proof." ))
     (when (eq coq-diffs 'on) (list "Show Proof Diffs."))
-    (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))))))))
+    (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))))))
 
 
 (defpacustom auto-adapt-printing-width t
-- 
cgit v1.2.3


From 3ab3f5efbbb724cb2e4aebc3c4d7bfdce4008896 Mon Sep 17 00:00:00 2001
From: Anaclet
Date: Mon, 25 May 2020 10:55:03 +0200
Subject: fix: backtrack wrong type argument

---
 coq/coq-syntax.el |  2 +-
 coq/coq.el        | 40 +++++++++++++++++++++-------------------
 2 files changed, 22 insertions(+), 20 deletions(-)

(limited to 'coq')

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 47869aed..5b8d8c48 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1305,7 +1305,7 @@ It is used:
 
 
 (defconst coq-show-proof-diffs-regexp
-  "\\bShow Proof\\(?: Diffs\\| Diffs removed\\)?\\.\\b")
+  "\\`Show Proof\\(?: Diffs\\| Diffs removed\\)?\\.\\'")
 
 (defconst coq-save-command-regexp
   ;; FIXME: The surrounding grouping parens are probably not needed.
diff --git a/coq/coq.el b/coq/coq.el
index 10aa07bf..9fc6e200 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -162,9 +162,9 @@ See also option `coq-hide-additional-subgoals'."
 
 (defcustom coq-show-proof-stepwise nil
   "Display the proof terms stepwise in the *response* buffer.
-  This option can be combined with option `coq-diffs'.
-  It is mostly useful in three window mode, see also
-  `proof-three-window-mode-policy' for details."
+This option can be combined with option `coq-diffs'.
+It is mostly useful in three window mode, see also
+`proof-three-window-mode-policy' for details."
 
   :type 'boolean
   :safe 'booleanp
@@ -1209,7 +1209,9 @@ Printing All set."
   "Return the list of commands to send to Coq after CMD
 if it is the last command of the action list.
 If CMD is tagged with 'empty-action-list then this function won't
-be called and no command will be sent to Coq."
+be called and no command will be sent to Coq.
+Note: the last command added if `coq-show-proof-stepwise' is set
+should match the `coq-show-proof-diffs-regexp'."
   (cond
    ((or
      ;; If closing a nested proof, Show the enclosing goal.
@@ -1219,11 +1221,11 @@ be called and no command will be sent to Coq."
      (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd)
           (> (length coq-last-but-one-proofstack) 0)))
     (list "Show."
-    (when coq-show-proof-stepwise
-        (or
-    (when (eq coq-diffs 'off) "Show Proof.")
-    (when (eq coq-diffs 'on) "Show Proof Diffs.")
-    (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
+          (when coq-show-proof-stepwise
+            (or
+             (when (eq coq-diffs 'off) "Show Proof.")
+             (when (eq coq-diffs 'on) "Show Proof Diffs.")
+             (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
    
    ((or
      ;; If we go back in the buffer and the number of abort is less than
@@ -1232,11 +1234,11 @@ be called and no command will be sent to Coq."
           (> (length coq-last-but-one-proofstack) coq--retract-naborts)))
     ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs
     (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")
-                                  (when coq-show-proof-stepwise
-                                    (or
-    (when (eq coq-diffs 'off) "Show Proof.")
-    (when (eq coq-diffs 'on) "Show Proof Diffs.")
-    (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
+          (when coq-show-proof-stepwise
+            (or
+             (when (eq coq-diffs 'off) "Show Proof.")
+             (when (eq coq-diffs 'on) "Show Proof Diffs.")
+             (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
 
    ((or
      ;; If we go back in the buffer and not in the above case, then only Unset
@@ -1251,11 +1253,11 @@ be called and no command will be sent to Coq."
      ;; If doing (not closing) a proof, Show Proof if need be
      (and (not (string-match-p coq-save-command-regexp-strict cmd))
           (> (length coq-last-but-one-proofstack) 0)))
-          (when coq-show-proof-stepwise
-              (or
-    (when (eq coq-diffs 'off) (list "Show Proof." ))
-    (when (eq coq-diffs 'on) (list "Show Proof Diffs."))
-    (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))))))
+    (when coq-show-proof-stepwise
+      (or
+       (when (eq coq-diffs 'off) (list "Show Proof." ))
+       (when (eq coq-diffs 'on) (list "Show Proof Diffs."))
+       (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))))))
 
 
 (defpacustom auto-adapt-printing-width t
-- 
cgit v1.2.3


From 8627fba2a20e42432de441391db2f35e3c48a952 Mon Sep 17 00:00:00 2001
From: Anaclet
Date: Thu, 28 May 2020 09:21:53 +0200
Subject: fix: backtrack for "Show Proof" disabled

---
 coq/coq.el | 44 +++++++++++++++++++++++++++++++-------------
 1 file changed, 31 insertions(+), 13 deletions(-)

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 9fc6e200..df7c5a66 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1220,12 +1220,17 @@ should match the `coq-show-proof-diffs-regexp'."
      ;; If user issued a printing option then t printing.
      (and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd)
           (> (length coq-last-but-one-proofstack) 0)))
-    (list "Show."
-          (when coq-show-proof-stepwise
-            (or
-             (when (eq coq-diffs 'off) "Show Proof.")
-             (when (eq coq-diffs 'on) "Show Proof Diffs.")
-             (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
+    (let ((showlist (list "Show.")))
+      (when coq-show-proof-stepwise
+        (add-to-list 'showlist
+                     (if (coq--post-v811) 
+                     (or
+                      (when (eq coq-diffs 'off) "Show Proof.")
+                      (when (eq coq-diffs 'on) "Show Proof Diffs.")
+                      (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))
+                     "Show Proof.")
+                     t))
+      showlist))
    
    ((or
      ;; If we go back in the buffer and the number of abort is less than
@@ -1233,12 +1238,23 @@ should match the `coq-show-proof-diffs-regexp'."
      (and (string-match-p "BackTo\\s-" cmd)
           (> (length coq-last-but-one-proofstack) coq--retract-naborts)))
     ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs
-    (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")
-          (when coq-show-proof-stepwise
-            (or
-             (when (eq coq-diffs 'off) "Show Proof.")
-             (when (eq coq-diffs 'on) "Show Proof Diffs.")
-             (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
+    ;; (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")
+    ;;       (when coq-show-proof-stepwise
+    ;;         (or
+    ;;          (when (eq coq-diffs 'off) "Show Proof.")
+    ;;          (when (eq coq-diffs 'on) "Show Proof Diffs.")
+    ;;          (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
+    (let ((showlist (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show."))))
+      (when coq-show-proof-stepwise
+        (add-to-list 'showlist
+                     (if (coq--post-v811) 
+                     (or
+                      (when (eq coq-diffs 'off) "Show Proof.")
+                      (when (eq coq-diffs 'on) "Show Proof Diffs." )
+                      (when (eq coq-diffs 'removed) "Show Proof Diffs removed."))
+                     "Show Proof.")
+                     t))
+      showlist))
 
    ((or
      ;; If we go back in the buffer and not in the above case, then only Unset
@@ -1254,10 +1270,12 @@ should match the `coq-show-proof-diffs-regexp'."
      (and (not (string-match-p coq-save-command-regexp-strict cmd))
           (> (length coq-last-but-one-proofstack) 0)))
     (when coq-show-proof-stepwise
+      (if (coq--post-v811) 
       (or
        (when (eq coq-diffs 'off) (list "Show Proof." ))
        (when (eq coq-diffs 'on) (list "Show Proof Diffs."))
-       (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))))))
+       (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))
+       (list "Show Proof."))))))
 
 
 (defpacustom auto-adapt-printing-width t
-- 
cgit v1.2.3


From 77fd293d631bc17afc18ab36ea5d0e0a28fa5f52 Mon Sep 17 00:00:00 2001
From: Anaclet
Date: Fri, 29 May 2020 10:42:15 +0200
Subject: Minor changes

---
 coq/coq.el | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index df7c5a66..efa60349 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1237,13 +1237,6 @@ should match the `coq-show-proof-diffs-regexp'."
      ;; the number of nested goals, then Unset Silent and Show the goal
      (and (string-match-p "BackTo\\s-" cmd)
           (> (length coq-last-but-one-proofstack) coq--retract-naborts)))
-    ;; "Set Diffs" always re-prints the proof context with (if enabled) diffs
-    ;; (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")
-    ;;       (when coq-show-proof-stepwise
-    ;;         (or
-    ;;          (when (eq coq-diffs 'off) "Show Proof.")
-    ;;          (when (eq coq-diffs 'on) "Show Proof Diffs.")
-    ;;          (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
     (let ((showlist (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show."))))
       (when coq-show-proof-stepwise
         (add-to-list 'showlist
-- 
cgit v1.2.3