fix: backtrack wrong type argument

3 files changed, 38 insertions, 34 deletions

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
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 1258c7f6..9e51d4fb 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1181,21 +1181,23 @@ 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)
-	     (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
-		 (string-match-p proof-show-proof-diffs-regexp (car (nth 1 (car (last proof-action-list)))))))))))
+	   (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)