fix: backtrack for "Show Proof" disabled

2 files changed, 52 insertions, 35 deletions

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
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 9e51d4fb..b9ac2b3c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1139,12 +1139,12 @@ contains only invisible elements for Prooftree synchronization."
                    (not (memq 'empty-action-list flags))
                    proof-shell-empty-action-list-command)
           (let* ((cmd (mapconcat 'identity (nth 1 item) " "))
-                (extra-cmds (apply proof-shell-empty-action-list-command (list cmd)))
-                ;; tag all new items with 'empty-action-list
-                (extra-items (mapcar (lambda (s) (proof-shell-action-list-item
-                                                  s 'proof-done-invisible
-                                                  (list 'invisible 'empty-action-list)))
-                                     extra-cmds)))
+                 (extra-cmds (apply proof-shell-empty-action-list-command (list cmd)))
+                 ;; tag all new items with 'empty-action-list
+                 (extra-items (mapcar (lambda (s) (proof-shell-action-list-item
+                                                   s 'proof-done-invisible
+                                                   (list 'invisible 'empty-action-list)))
+                                      extra-cmds)))
             ;; action-list should be empty at this point
             (setq proof-action-list (append extra-items proof-action-list))))
 
@@ -1181,23 +1181,22 @@ contains only invisible elements for Prooftree synchronization."
 	;; process the delayed callbacks now
 	(mapc 'proof-shell-invoke-callback cbitems)
 
-	 (unless (or proof-action-list proof-second-action-list-active)
+	(unless (or proof-action-list proof-second-action-list-active)
 					; release lock, cleanup
-	   (proof-release-lock)
-	   (proof-detach-queue)
-	   (unless flags ; hint after a batch of scripting
-	     (pg-processing-complete-hint))
-	   (pg-finish-tracing-display))
-
-	 
-	 (and (not proof-second-action-list-active)
-	      (let ((last-command  (car (nth 1 (car (last proof-action-list))))))
-	      (or (null proof-action-list)
-		  (cl-every
-		   (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item)))
-		   proof-action-list)
-		  ;; If the last command in proof-action-list is a "Show Proof" form then return t
-		  (when last-command (string-match-p proof-show-proof-diffs-regexp last-command)))))))))
+	  (proof-release-lock)
+	  (proof-detach-queue)
+	  (unless flags ; hint after a batch of scripting
+	    (pg-processing-complete-hint))
+	  (pg-finish-tracing-display))
+
+	(and (not proof-second-action-list-active) 
+	     (let ((last-command  (car (nth 1 (car (last proof-action-list))))))
+	       (or (null proof-action-list)
+	 	   (cl-every
+	 	    (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item)))
+	 	    proof-action-list)
+	 	   ;; If the last command in proof-action-list is a "Show Proof" form then return t
+	 	   (when last-command (string-match-p proof-show-proof-diffs-regexp last-command)))))))))
 
 
 (defun proof-shell-insert-loopback-cmd  (cmd)