diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-06-13 10:59:04 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-06-13 10:59:04 +0000 |
| commit | c46355d3400389ad347e58036de408b678f0c3ea (patch) | |
| tree | f13da79686d1ead4dfa7542f9e95f68738aa6adf /generic/proof-config.el | |
| parent | f3f1e0021282bc89010cf5e5aeb5ca21c58994e3 (diff) | |
Docs
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index f54363a4..dd1d05b4 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1261,7 +1261,14 @@ will be attempted." (defcustom proof-kill-goal-command "" "Command to kill the currently open goal. -You must set this (perhaps to a no-op) for script management to work." +If this is set to nil, PG will expect proof-find-and-forget-fn +to do all the work of retracting to an arbitrary point in a file. +Otherwise, the generic split-phase mechanism will be used: + + 1. If inside an unclosed proof, use proof-count-undos. + 2. If retracting to before an unclosed proof, use + proof-kill-goal-command, followed by proof-find-and-forget-fn + if necessary." :type 'string :group 'proof-script) |