diff options
| author | Erik Martin-Dorel | 2020-05-29 19:56:44 +0200 |
|---|---|---|
| committer | GitHub | 2020-05-29 19:56:44 +0200 |
| commit | 5ba7aee8a8996b8219a6e9dbde645e53684afbca (patch) | |
| tree | 297503b50c51cc04a60609e42e6140d4ed2177de /generic | |
| parent | 0bfd208037646a1e1871dae9fc6fc6be0f7bd39c (diff) | |
| parent | 9c82b71d396b425337592f96f2e9b6a1d97be0c0 (diff) | |
Merge pull request #490 from ProofGeneral/feature/487
Improve PG support of Show Proof (Diffs):
Display the proof terms stepwise in the *response* buffer.
Close #487
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 5 | ||||
| -rw-r--r-- | generic/proof-shell.el | 25 |
2 files changed, 19 insertions, 11 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 8d539191..9d352548 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -399,6 +399,11 @@ NB: This setting is not used for matching output from the prover." :type 'regexp :group 'proof-script) +(defcustom proof-show-proof-diffs-regexp nil + "Matches all \"Show Proof\" forms (specific to the Coq prover)." + :type 'regexp + :group 'proof-script) + (defcustom proof-save-with-hole-regexp nil "Regexp which matches a command to save a named theorem. The name of the theorem is built from the variable diff --git a/generic/proof-shell.el b/generic/proof-shell.el index a0e80fa7..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)))) @@ -1189,11 +1189,14 @@ contains only invisible elements for Prooftree synchronization." (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))))))) + (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) |