diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-10-13 15:21:41 +0200 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-10-13 15:21:41 +0200 |
commit | efb54b9098d665fd58e99c42f53afd7e49a36c70 (patch) | |
tree | 9af31abb8b95f6a717788b5c517ee8f803d0bb17 /generic/proof-config.el | |
parent | 14b8d0e24ef48032885018b4020969593477ee26 (diff) |
proof-retract-command-hook added + more auto adjust width in coq mode.
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." |