diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 13 | ||||
| -rw-r--r-- | generic/proof-script.el | 1 |
2 files changed, 14 insertions, 0 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 43ca9a86..fc2dca86 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1616,6 +1616,19 @@ it is added to the queue of commands." :type '(repeat function) :group 'proof-shell) +(defcustom proof-assert-command-hook nil + "Hooks run before asserting a command (or a set of commands). +Can be used to insert commands before any (set of) input sent +by the user. It is run by `proof-assert-until-point'. + +WARNING: don't call `proof-assert-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).") + (defcustom proof-script-preprocess nil "Function to pre-process (SPAN STRING) taken from proof script." :type 'function diff --git a/generic/proof-script.el b/generic/proof-script.el index fbd8c2b1..338318e7 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1912,6 +1912,7 @@ Assumes that point is at the end of a command." (setq semis (cdr semis))) (if (null semis) ; maybe inside a string or something. (error "I can't find any complete commands to process!")) + (run-hooks 'proof-assert-command-hook) ;; sneak commands (real ones with a prompt) (proof-assert-semis semis displayflags))) (defun proof-assert-electric-terminator () |