diff options
| author | David Aspinall | 1999-11-14 12:20:04 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-11-14 12:20:04 +0000 |
| commit | 056b75cd2baac63ded2375eea02738249c9dddb8 (patch) | |
| tree | 4aee816908a55cc9f79997e3243a49afa45c9d65 /generic/proof-config.el | |
| parent | 5dd305339e5b4f1ab8883349301916a3d2ac118f (diff) | |
Many robustness improvements for error and interrupt handling:
- Introduce proof-shell-error-or-interrupt-seen flag set after an error
or interrupt was seen (in fact, on every call to proof-release-lock).
Examine it in proof-activate-scripting to see whether hooks succeeded
in activating scripting.
- Test in the shell filter for the lock being held yet nothing in the
action list, and clear the lock if so. Gets rid of repetetive
proof-shell-busy messages when the queue is empty (for errors during
development, or nasty uses of C-g)
- Add a timeout to proof-shell-wait (not used yet)
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index cf03c487..4f0e05f1 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1353,9 +1353,11 @@ its friends configured in the function proof-shell-start." :type '(repeat function) :group 'proof-shell) -(defcustom proof-shell-handle-error-hook +(defcustom proof-shell-handle-error-or-interrupt-hook '(proof-goto-end-of-locked-if-pos-not-visible-in-window) - "Hooks run after an error has been reported in the response buffer." + "Run after an error or interrupt has been reported in the response buffer. +Hook functions may inspect `proof-shell-error-or-interrupt-seen' to +determine whether the cause was an error or interrupt." :type '(repeat function) :group 'proof-shell) |