diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 5 | ||||
| -rw-r--r-- | generic/proof-shell.el | 7 |
2 files changed, 10 insertions, 2 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 8d539191..16cdae93 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-diffs-regexp nil + "Matches all Show Proof form" + :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..b6bf9225 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1615,9 +1615,12 @@ 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) - (setq proof-shell-last-output-kind + ;; (if (and (string-match proof-show-diffs-regexp (car cmd)) + ;; (memq 'empty-action-list flags)) + ;; (setq proof-shell-last-output-kind 'response) ;; only display result for last output - (proof-shell-handle-delayed-output))) + (setq proof-shell-last-output-kind (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))))) |