diff options
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index fc2dca86..b4898a35 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1627,7 +1627,24 @@ would loop forever. Example of use: Insert a command to adapt printing width. Note that `proof-shell-insert-hook' may be use instead (see lego mode) if no more prompt will be displayed (see -`proof-shell-insert-hook' for details).") +`proof-shell-insert-hook' for details)." + :type '(repeat function) + :group 'proof-shell) + +(defcustom proof-retract-command-hook nil + "Hooks run before retracting a command (or a set of commands). +Can be used to insert commands. It is run by +`proof-retract-until-point'. + +WARNING: don't call `proof-retract-until-point' in this hook, you +would loop forever. + +Example of use: Insert a command to adapt printing width. Note +that `proof-shell-insert-hook' may be use instead (see lego mode) +if no more prompt will be displayed (see +`proof-shell-insert-hook' for details)." + :type '(repeat function) + :group 'proof-shell) (defcustom proof-script-preprocess nil "Function to pre-process (SPAN STRING) taken from proof script." |