diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-10-01 15:07:07 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-10-01 15:07:07 +0000 |
| commit | 1604db92ae0d21b58caafb481aef73570056a122 (patch) | |
| tree | d97fd823c24b0eb2a1dce8612fc19335f58f67af /generic/proof-shell.el | |
| parent | 7649ff839e9ee7ddbb41b53c30a96c5fbf8316d8 (diff) | |
proof-shell-handle-error-or-interrupt-hook: only run if ordinary scripting input (no non-nil flags in queue)
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 445107b7..aaff5673 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -597,7 +597,11 @@ didn't cause prover output." "Take action on errors or interrupts. ERR-OR-INT is a flag, 'error or 'interrupt. This is a subroutine of `proof-shell-handle-error-or-interrupt'. -Must be called with proof shell buffer current." +Must be called with proof shell buffer current. + +This function invokes `proof-shell-handle-error-or-interrupt-hook' +unless the FLAGS for the command are non-nil (indicating errors +are ignored somehow)." (unless proof-shell-quiet-errors (beep)) (let* ((fatalitem (car-safe proof-action-list)) @@ -613,8 +617,9 @@ Must be called with proof shell buffer current." (unless flags ;; Give a hint about C-c C-`. (NB: approximate test) (if (pg-response-has-error-location) - (pg-next-error-hint))) - (run-hooks 'proof-shell-handle-error-or-interrupt-hook))) + (pg-next-error-hint)) + ;; Run hooks for additional effects, e.g. highlight or moving pointer + (run-hooks 'proof-shell-handle-error-or-interrupt-hook)))) (defun proof-goals-pos (span maparg) "Given a span, return the start of it if corresponds to a goal, nil otherwise." |