diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-02-09 20:18:39 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-02-09 20:18:39 +0000 |
| commit | 587f211719f8d4c273cd82a4100ab19a796c2946 (patch) | |
| tree | 0e38b1b81f681716514c354bc9aeca6343c92e9e | |
| parent | c8752c5923da2944d43db282306dd26a3a5c093c (diff) | |
Doc for proof-shell-pre-interrupt-hook
| -rw-r--r-- | doc/ProofGeneral.texi | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index ec7a9417..5bebbad1 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3996,6 +3996,15 @@ Hook functions may inspect @samp{@code{proof-shell-error-or-interrupt-seen}} to determine whether the cause was an error or interrupt. @end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-pre-interrupt-hook +@defvar proof-shell-pre-interrupt-hook +Run immediately after @samp{@code{comint-interrupt-subjob}} is called.@* +This hook is added to allow customization for Poly/ML and other +systems where the system queries the user before returning to +the top level. For Poly/ML it can be used to send the string "f", +for example. +@end defvar + @c TEXI DOCSTRING MAGIC: proof-shell-process-output-system-specific @defvar proof-shell-process-output-system-specific Set this variable to handle system specific output.@* |