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

3 files changed, 43 insertions, 5 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 3ba0487a..c62f84b1 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1120,13 +1120,22 @@ flag Printing All set."
 (eval-when (compile)
   (defvar coq-auto-adapt-printing-width nil)); defpacustom
 
+;; Since Printing Width is a synchronized option in coq (?) it is retored
+;; silently to a previous value when retracting. So we reset the stored width
+;; when retracting, so that it will be auto-adapted at the next command. Not
+;; perfect: we have to forward one step to see the effect.
+
+;; FIXME: hopefully this will eventually become a non synchronized option and
+;; we can remove this.
 (defun coq-auto-adapt-printing-width-switch ()
   "Function called when toggling `auto-adapt-printing-width'"
   (if coq-auto-adapt-printing-width
-      (add-hook 'proof-assert-command-hook 'coq-adapt-printing-width)
-    (remove-hook 'proof-assert-command-hook 'coq-adapt-printing-width)))
+      (progn
+        (add-hook 'proof-assert-command-hook 'coq-adapt-printing-width)
+        (add-hook 'proof-retract-command-hook 'coq-reset-printing-width))
+    (remove-hook 'proof-assert-command-hook 'coq-adapt-printing-width)
+    (remove-hook 'proof-retract-command-hook 'coq-reset-printing-width)))
 
-(add-hook 'proof-assert-command-hook 'coq-adapt-printing-width)
 
 (defpacustom auto-adapt-printing-width t
   "If non-nil, adapt automatically printing width of goals window.
@@ -1140,11 +1149,21 @@ width is synchronized by coq (?!)."
   :group 'coq
   :eval (coq-auto-adapt-printing-width-switch))
 
+;; this initiates aut adapt printing width at start, by reading the config var.
+;; Let us put this at the end of hooks to have a chance to read local variables
+;; first.
+(add-hook 'coq-mode-hook 'coq-auto-adapt-printing-width-switch t)
+
 (defvar coq-shell-current-line-width nil
   "Current line width of the Coq printing width.
 Its value will be updated whenever a command is sent if
 necessary.")
 
+;; Resetting the known printing width (for when we don't know it, for example
+;; when retracting.
+(defun coq-reset-printing-width ()
+  (setq coq-shell-current-line-width nil))
+
 (defun coq-goals-window-width ()
   (let*
       ((goals-wins (get-buffer-window-list proof-goals-buffer))
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!"))))))