Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Improve PG support of Show Proof Diffs #490

Merged
merged 13 commits into from
May 29, 2020
Merged

Improve PG support of Show Proof Diffs #490

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
8e12eee
First try for feature #487
CyrilAnac May 11, 2020
ecb4747
All case for Show and regex variable
CyrilAnac May 14, 2020
aba3f2b
Fix name clash & rephrase some strings
erikmd May 15, 2020
04aff70
WIP for #487
CyrilAnac May 18, 2020
22681a3
Apply reviews of @erikmd
CyrilAnac May 20, 2020
ff9b5b1
test: Add regression test (currently failing)
erikmd May 20, 2020
411ebb2
fix: Do "Show Proof…" (with "?Goal") as soon as the proof is started
erikmd May 20, 2020
3ab3f5e
fix: backtrack wrong type argument
CyrilAnac May 25, 2020
8627fba
fix: backtrack for "Show Proof" disabled
CyrilAnac May 28, 2020
5b1b8ac
Add tests and flags system
CyrilAnac May 28, 2020
cc4b4f6
Fix the test 081
CyrilAnac May 28, 2020
77fd293
Minor changes
CyrilAnac May 29, 2020
9c82b71
refactor: Remove unneeded coq-should-response
erikmd May 29, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
fix: backtrack for "Show Proof" disabled
  • Loading branch information
@CyrilAnac
CyrilAnac committed May 29, 2020
commit 8627fba2a20e42432de441391db2f35e3c48a952
44 changes: 31 additions & 13 deletions coq/coq.el
View file
Open in desktop
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.")))))
CyrilAnac marked this conversation as resolved.
Show resolved Hide resolved
(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
Open in desktop
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