diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-28 08:40:57 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-28 08:40:57 +0000 |
| commit | 4b2801a521f7365f8a3833fa9805828792dac853 (patch) | |
| tree | 1c9159ba41b75b362370307a098e3c86821dafcc /generic/proof-config.el | |
| parent | 07c7e94620921a826ac07363bf49f35cff0e6bc9 (diff) | |
Functions find-and-forget and count-undos now return lists of commands
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 23dae667..de9f73e4 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -599,7 +599,7 @@ save commands, so don't use that if your prover has save commands." :group 'proof-script) (defcustom proof-count-undos-fn 'proof-generic-count-undos - "Function to calculate a command to issue undos to reach a target span. + "Function to calculate a list of command to undo to reach a target span. The function takes a span as an argument, and should return a string which is the command to undo to the target span. The target is guaranteed to be within the current (open) proof. @@ -611,7 +611,7 @@ settings `proof-non-undoables-regexp' and :group 'proof-script) (defcustom proof-find-and-forget-fn 'proof-generic-find-and-forget - "Function that returns a command to forget back to before its argument span. + "Function to return list of commands to forget to before its argument span. This setting is used to for retraction (undoing) in proof scripts. It should undo the effect of all settings between its target span |