diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2011-04-13 11:24:52 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2011-04-13 11:24:52 +0000 |
| commit | 73617c15286def069e3b0a49c37805c42ccb6e56 (patch) | |
| tree | 5514e5e34d16b26fd937dde5953ee1842d4c3166 /generic/proof-config.el | |
| parent | 3884744c21350c79390888cab39e9cf82dcbf487 (diff) | |
proof-shell-insert-hook: Clean docstring, addressing #396.
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 10 |
1 files changed, 6 insertions, 4 deletions
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 |