Skip to content

Commit

Permalink
fix: backtrack for "Show Proof" disabled
Browse files Browse the repository at this point in the history
  • Loading branch information
@CyrilAnac
CyrilAnac committed May 29, 2020
1 parent 3ab3f5e commit 8627fba
Show file tree
Hide file tree
Showing 2 changed files with 52 additions and 35 deletions.
44 changes: 31 additions & 13 deletions coq/coq.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1220,25 +1220,41 @@ 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
;; 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.")))))
;; (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
Expand All @@ -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
Expand Down
43 changes: 21 additions & 22 deletions generic/proof-shell.el
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))))

Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit 8627fba

Please sign in to comment.