diff options
| author | Cyril Anaclet | 2020-05-20 14:19:14 +0200 |
|---|---|---|
| committer | Anaclet | 2020-05-29 11:05:58 +0200 |
| commit | 22681a3caf2c8f45700585ea74dffbf48bb2ac19 (patch) | |
| tree | 40570f1694889d27d66e3a4d9e5f4019bb06995e /generic | |
| parent | 04aff704f3d13452bc5c52ff860c5ab564539632 (diff) | |
Apply reviews of @erikmd
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 2 | ||||
| -rw-r--r-- | generic/proof-shell.el | 14 |
2 files changed, 7 insertions, 9 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index ce72c76c..9d352548 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -400,7 +400,7 @@ NB: This setting is not used for matching output from the prover." :group 'proof-script) (defcustom proof-show-proof-diffs-regexp nil - "Matches all Show Proof form" + "Matches all \"Show Proof\" forms (specific to the Coq prover)." :type 'regexp :group 'proof-script) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 8f23608a..1258c7f6 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1126,7 +1126,7 @@ contains only invisible elements for Prooftree synchronization." ;; but we delay this until sending the next command, attempting ;; to parallelize prover and Emacs somewhat. (PG 4.0 change) - (setq proof-action-list (cdr proof-action-list)) + (setq proof-action-list (cdr proof-action-list)) (setq cbitems (cons item (proof-shell-slurp-comments))) @@ -1194,7 +1194,8 @@ contains only invisible elements for Prooftree synchronization." (cl-every (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) proof-action-list) - (string= (car (nth 1 item)) "Show."))))))) + ;; 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))))))))))) (defun proof-shell-insert-loopback-cmd (cmd) @@ -1616,12 +1617,9 @@ by the filter is to send the next command from the queue." (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) (if (proof-shell-exec-loop) - ;; (if (and (string-match proof-show-diffs-regexp (car cmd)) - ;; (memq 'empty-action-list flags)) - ;; (setq proof-shell-last-output-kind 'response) + (setq proof-shell-last-output-kind ;; only display result for last output - (setq proof-shell-last-output-kind (proof-shell-handle-delayed-output))) - ;; + (proof-shell-handle-delayed-output))) ;; send output to the proof tree visualizer (if proof-tree-external-display (proof-tree-handle-delayed-output old-proof-marker cmd flags span))))) @@ -1716,7 +1714,7 @@ i.e., 'goals or 'response." (buffer-substring-no-properties rstart gmark))) ;; display goals output second so it persists in 2-pane mode (unless (memq 'no-goals-display flags) - (pg-goals-display proof-shell-last-goals-output t)) + (pg-goals-display proof-shell-last-goals-output both)) ;; indicate a goals output has been given 'goals)) |