diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 19 | ||||
| -rw-r--r-- | generic/proof-script.el | 4 |
2 files changed, 21 insertions, 2 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." diff --git a/generic/proof-script.el b/generic/proof-script.el index 338318e7..e65d2fc9 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2238,7 +2238,9 @@ query saves here." (backward-char) (setq span (span-at (point) 'type))) (if span - (proof-retract-target span undo-action displayflags) + (progn + (run-hooks 'proof-retract-command-hook) ;; sneak commands (real ones with a prompt) + (proof-retract-target span undo-action displayflags)) ;; something wrong (proof-debug "proof-retract-until-point: couldn't find a span!")))))) |