diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-10 23:04:40 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-10 23:04:40 +0000 |
| commit | ee91c3f2f1dd5f2f731db385134f38726b37b7ca (patch) | |
| tree | d9cb381181a462fdbfab57f7e1f0d4e67ce567b2 /generic/proof-config.el | |
| parent | a060c0dc046e526f8bf88b512e3c7c27e93421f8 (diff) | |
Experimental changes to queue several commands at once and to allow pre-processing of commands when they're queued from script
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." |