aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-shell.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1998-12-07 17:29:00 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1998-12-07 17:29:00 +0000
commit3bd5aa94de7f70921ddb570c8ee3281e7d740f78 (patch)
tree5bf2a4d78b3309217574e939f091beca0116d446 /generic/proof-shell.el
parent4989a863c3cf0593674a183e09ed11dff6aa38a5 (diff)
Added proof-shell-preprocess-command for Paul Callaghan.
Diffstat (limited to 'generic/proof-shell.el')
-rw-r--r--generic/proof-shell.el6
1 files changed, 6 insertions, 0 deletions
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)