From 587f211719f8d4c273cd82a4100ab19a796c2946 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 9 Feb 2000 20:18:39 +0000 Subject: Doc for proof-shell-pre-interrupt-hook --- doc/ProofGeneral.texi | 9 +++++++++ 1 file changed, 9 insertions(+) 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.@* -- cgit v1.2.3