aboutsummaryrefslogtreecommitdiff
path: root/generic
diff options
context:
space:
mode:
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-config.el6
-rw-r--r--generic/proof-shell.el6
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)