From 73617c15286def069e3b0a49c37805c42ccb6e56 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 13 Apr 2011 11:24:52 +0000 Subject: proof-shell-insert-hook: Clean docstring, addressing #396. --- generic/proof-config.el | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'generic/proof-config.el') diff --git a/generic/proof-config.el b/generic/proof-config.el index 8ce2c86c..b5289234 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1567,13 +1567,15 @@ Before sending `string', it will be stripped of carriage returns. Additionally, the hook can examine the variable `action'. It will be a symbol, set to the callback command which is executed in the proof shell filter once `string' has been processed. The `action' variable -suggests what class of command is about to be inserted: +suggests what class of command is about to be inserted, the first two +are normally the ones of interest: - 'proof-done-invisible A non-scripting command 'proof-done-advancing A \"forward\" scripting command 'proof-done-retracting A \"backward\" scripting command - 'init-cmd Initialization command sent to prover - 'interactive-input Special interactive input direct to prover + 'proof-done-invisible A non-scripting command + 'proof-shell-set-silent Indicates prover output has been surpressed + 'proof-shell-clear-silent Indicates prover output has been restored + 'init-cmd Early initialization command sent to prover Caveats: You should be very careful about setting this hook. Proof General relies on a careful synchronization with the process between -- cgit v1.2.3