Skip to content

Commit bd33961

Browse files
CyrilAnacCyrilAnac
committed
fix: backtrack for "Show Proof" disabled
1 parent 9fedf57 commit bd33961

File tree

2 files changed

+52
-35
lines changed

2 files changed

+52
-35
lines changed

‎coq/coq.el

+31-13
Original file line numberDiff line numberDiff line change
@@ -1215,25 +1215,41 @@ should match the `coq-show-proof-diffs-regexp'."
12151215
;; If user issued a printing option then t printing.
12161216
(and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd)
12171217
(> (length coq-last-but-one-proofstack) 0)))
1218-
(list "Show."
1219-
(when coq-show-proof-stepwise
1220-
(or
1221-
(when (eq coq-diffs 'off) "Show Proof.")
1222-
(when (eq coq-diffs 'on) "Show Proof Diffs.")
1223-
(when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
1218+
(let ((showlist (list "Show.")))
1219+
(when coq-show-proof-stepwise
1220+
(add-to-list 'showlist
1221+
(if (coq--post-v811)
1222+
(or
1223+
(when (eq coq-diffs 'off) "Show Proof.")
1224+
(when (eq coq-diffs 'on) "Show Proof Diffs.")
1225+
(when (eq coq-diffs 'removed) "Show Proof Diffs removed."))
1226+
"Show Proof.")
1227+
t))
1228+
showlist))
12241229

12251230
((or
12261231
;; If we go back in the buffer and the number of abort is less than
12271232
;; the number of nested goals, then Unset Silent and Show the goal
12281233
(and (string-match-p "BackTo\\s-" cmd)
12291234
(> (length coq-last-but-one-proofstack) coq--retract-naborts)))
12301235
;; "Set Diffs" always re-prints the proof context with (if enabled) diffs
1231-
(list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")
1232-
(when coq-show-proof-stepwise
1233-
(or
1234-
(when (eq coq-diffs 'off) "Show Proof.")
1235-
(when (eq coq-diffs 'on) "Show Proof Diffs.")
1236-
(when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
1236+
;; (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")
1237+
;; (when coq-show-proof-stepwise
1238+
;; (or
1239+
;; (when (eq coq-diffs 'off) "Show Proof.")
1240+
;; (when (eq coq-diffs 'on) "Show Proof Diffs.")
1241+
;; (when (eq coq-diffs 'removed) "Show Proof Diffs removed.")))))
1242+
(let ((showlist (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show."))))
1243+
(when coq-show-proof-stepwise
1244+
(add-to-list 'showlist
1245+
(if (coq--post-v811)
1246+
(or
1247+
(when (eq coq-diffs 'off) "Show Proof.")
1248+
(when (eq coq-diffs 'on) "Show Proof Diffs." )
1249+
(when (eq coq-diffs 'removed) "Show Proof Diffs removed."))
1250+
"Show Proof.")
1251+
t))
1252+
showlist))
12371253

12381254
((or
12391255
;; If we go back in the buffer and not in the above case, then only Unset
@@ -1249,10 +1265,12 @@ should match the `coq-show-proof-diffs-regexp'."
12491265
(and (not (string-match-p coq-save-command-regexp-strict cmd))
12501266
(> (length coq-last-but-one-proofstack) 0)))
12511267
(when coq-show-proof-stepwise
1268+
(if (coq--post-v811)
12521269
(or
12531270
(when (eq coq-diffs 'off) (list "Show Proof." ))
12541271
(when (eq coq-diffs 'on) (list "Show Proof Diffs."))
1255-
(when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))))))
1272+
(when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))
1273+
(list "Show Proof."))))))
12561274

12571275

12581276
(defpacustom auto-adapt-printing-width t

‎generic/proof-shell.el

+21-22
Original file line numberDiff line numberDiff line change
@@ -1139,12 +1139,12 @@ contains only invisible elements for Prooftree synchronization."
11391139
(not (memq 'empty-action-list flags))
11401140
proof-shell-empty-action-list-command)
11411141
(let* ((cmd (mapconcat 'identity (nth 1 item) " "))
1142-
(extra-cmds (apply proof-shell-empty-action-list-command (list cmd)))
1143-
;; tag all new items with 'empty-action-list
1144-
(extra-items (mapcar (lambda (s) (proof-shell-action-list-item
1145-
s 'proof-done-invisible
1146-
(list 'invisible 'empty-action-list)))
1147-
extra-cmds)))
1142+
(extra-cmds (apply proof-shell-empty-action-list-command (list cmd)))
1143+
;; tag all new items with 'empty-action-list
1144+
(extra-items (mapcar (lambda (s) (proof-shell-action-list-item
1145+
s 'proof-done-invisible
1146+
(list 'invisible 'empty-action-list)))
1147+
extra-cmds)))
11481148
;; action-list should be empty at this point
11491149
(setq proof-action-list (append extra-items proof-action-list))))
11501150

@@ -1181,23 +1181,22 @@ contains only invisible elements for Prooftree synchronization."
11811181
;; process the delayed callbacks now
11821182
(mapc 'proof-shell-invoke-callback cbitems)
11831183

1184-
(unless (or proof-action-list proof-second-action-list-active)
1184+
(unless (or proof-action-list proof-second-action-list-active)
11851185
; release lock, cleanup
1186-
(proof-release-lock)
1187-
(proof-detach-queue)
1188-
(unless flags ; hint after a batch of scripting
1189-
(pg-processing-complete-hint))
1190-
(pg-finish-tracing-display))
1191-
1192-
1193-
(and (not proof-second-action-list-active)
1194-
(let ((last-command (car (nth 1 (car (last proof-action-list))))))
1195-
(or (null proof-action-list)
1196-
(cl-every
1197-
(lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item)))
1198-
proof-action-list)
1199-
;; If the last command in proof-action-list is a "Show Proof" form then return t
1200-
(when last-command (string-match-p proof-show-proof-diffs-regexp last-command)))))))))
1186+
(proof-release-lock)
1187+
(proof-detach-queue)
1188+
(unless flags ; hint after a batch of scripting
1189+
(pg-processing-complete-hint))
1190+
(pg-finish-tracing-display))
1191+
1192+
(and (not proof-second-action-list-active)
1193+
(let ((last-command (car (nth 1 (car (last proof-action-list))))))
1194+
(or (null proof-action-list)
1195+
(cl-every
1196+
(lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item)))
1197+
proof-action-list)
1198+
;; If the last command in proof-action-list is a "Show Proof" form then return t
1199+
(when last-command (string-match-p proof-show-proof-diffs-regexp last-command)))))))))
12011200

12021201

12031202
(defun proof-shell-insert-loopback-cmd (cmd)

0 commit comments

Comments
 (0)