diff options
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 360581b9..e80ade04 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1662,10 +1662,19 @@ stripped of carriage returns before being sent. Example uses: LEGO uses this hook for setting the pretty printer width if the window width has changed; -Plastic uses it to remove literate-style markup from `string'." +Plastic uses it to remove literate-style markup from `string'. + +See also `proof-script-preprocess' which can munge text when +it is added to the queue of commands." :type '(repeat function) :group 'proof-shell) +(defcustom proof-script-preprocess nil + "Function to pre-process (SPAN STRING) taken from proof script." + :type 'function + :group 'proof-shell) + + (defcustom proof-shell-handle-delayed-output-hook '(proof-pbp-focus-on-first-goal) "Hooks run after new output has been displayed in goals or response buffer." |