diff options
| author | David Aspinall | 1998-12-07 17:29:00 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-12-07 17:29:00 +0000 |
| commit | 3bd5aa94de7f70921ddb570c8ee3281e7d740f78 (patch) | |
| tree | 5bf2a4d78b3309217574e939f091beca0116d446 /generic | |
| parent | 4989a863c3cf0593674a183e09ed11dff6aa38a5 (diff) | |
Added proof-shell-preprocess-command for Paul Callaghan.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 6 | ||||
| -rw-r--r-- | generic/proof-shell.el | 6 |
2 files changed, 12 insertions, 0 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 636f1f1f..1322b1a1 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -889,6 +889,12 @@ output format." :type '(cons (function function)) :group 'proof-shell) +(defcustom proof-shell-preprocess-command nil + "Any preprocessing required for a command, e.g. stripping comments. +This function will be applied to each string sent to the process." + :type 'function + :group 'proof-shell) + diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 8e1d1dc2..478fa103 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -839,6 +839,12 @@ proof-start-queue and proof-shell-exec-loop." ;; should not have any CRs. (run-hooks 'proof-shell-insert-hook) + ;; This hook added for Paul Callaghan's instantiation, + ;; to remove extra markup used for his "literate" + ;; style of input. + (and proof-shell-preprocess-command + (setq string (funcall proof-shell-preprocess-command string))) + (insert string) (set-marker proof-marker (point)) (insert proof-shell-insert-space-fudge) |