proof-retract-command-hook added + more auto adjust width in coq mode.

2 files changed, 21 insertions, 2 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index fc2dca86..b4898a35 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1627,7 +1627,24 @@ 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).")
+`proof-shell-insert-hook' for details)."
+  :type '(repeat function)
+  :group 'proof-shell)
+
+(defcustom proof-retract-command-hook nil
+  "Hooks run before retracting a command (or a set of commands).
+Can be used to insert commands. It is run by
+`proof-retract-until-point'.
+
+WARNING: don't call `proof-retract-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)."
+  :type '(repeat function)
+  :group 'proof-shell)
 
 (defcustom proof-script-preprocess nil
   "Function to pre-process (SPAN STRING) taken from proof script."
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 338318e7..e65d2fc9 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2238,7 +2238,9 @@ query saves here."
 	  (backward-char)
 	  (setq span (span-at (point) 'type)))
 	(if span
-	    (proof-retract-target span undo-action displayflags)
+	    (progn
+	      (run-hooks 'proof-retract-command-hook) ;; sneak commands (real ones with a prompt)
+	      (proof-retract-target span undo-action displayflags))
 	  ;; something wrong
 	  (proof-debug
 	   "proof-retract-until-point: couldn't find a span!"))))))