From 14b8d0e24ef48032885018b4020969593477ee26 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 12 Oct 2015 20:49:05 +0200 Subject: proof-assert-command-hook added + Auto adjust width in coq mode. This hook was missing, it allows to send complete commands before the (set of) command(s) sent by the user. It shall be used when proof-shell-insert-hook cannot be used (because of multiple prompts appearing). --- generic/proof-config.el | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'generic/proof-config.el') diff --git a/generic/proof-config.el b/generic/proof-config.el index 43ca9a86..fc2dca86 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1616,6 +1616,19 @@ it is added to the queue of commands." :type '(repeat function) :group 'proof-shell) +(defcustom proof-assert-command-hook nil + "Hooks run before asserting a command (or a set of commands). +Can be used to insert commands before any (set of) input sent +by the user. It is run by `proof-assert-until-point'. + +WARNING: don't call `proof-assert-until-point' in this hook, you +would loop forever. + +Example of use: Insert a command to adapt printing width. Note +that `proof-shell-insert-hook' may be use instead (see lego mode) +if no more prompt will be displayed (see +`proof-shell-insert-hook' for details).") + (defcustom proof-script-preprocess nil "Function to pre-process (SPAN STRING) taken from proof script." :type 'function -- cgit v1.2.3