branch: elpa/proof-general
commit d2d899b742638257c6e5fbd451c0dc1d9593dacb
Author: Pierre Courtieu <pierre.court...@cnam.fr>
Commit: Pierre Courtieu <pierre.court...@cnam.fr>
Fix #608. PG not auto adapting window width.
The option setting was flawed. A recent code cleaning revealed it.
Now the hooks are set once and forall correctly and obey the setting.
---
ci/coq-tests.el | 4 +++-
coq/coq.el | 47 +++++++++++++++--------------------------------
2 files changed, 18 insertions(+), 33 deletions(-)
diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index fb5635f..acea3e7 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -133,7 +133,9 @@ then evaluate the BODY function and finally tear-down (exit
Coq)."
;;; For info on macros: https://mullikine.github.io/posts/macro-tutorial
;;; (pp (macroexpand '(macro args)))
(save-excursion
- (let* ((openfile (or file
+ (let* (;; avoids bad width detection in batch mode
+ (coq-auto-adapt-printing-width nil)
+ (openfile (or file
(concat (make-temp-file coq-test-file-prefix) ".v")))
;; if FILE is nil, create a temporary Coq file, removed in the end
(rmfile (unless file openfile))
diff --git a/coq/coq.el b/coq/coq.el
index 84ce891..a112516 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1172,9 +1172,6 @@ Printing All set."
(interactive)
(coq-ask-do-show-all "Show goal number" "Show" t))
-;; Check
-(defvar coq-auto-adapt-printing-width); 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
@@ -1182,15 +1179,9 @@ Printing All set."
;; FIXME: hopefully this will eventually become a non synchronized option and
;; we can remove this.
-(defun coq-set-auto-adapt-printing-width (&optional _symb val); args are for
:set compatibility
- "Function called when setting `auto-adapt-printing-width'."
- (setq coq-auto-adapt-printing-width val)
- (if coq-auto-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)))
+;; This obeyx coq-auto-adapt-printing-width
+(add-hook 'proof-assert-command-hook #'coq-adapt-printing-width)
+(add-hook 'proof-retract-command-hook #'coq-reset-printing-width)
(defun coq--show-proof-stepwise-cmds ()
(when coq-show-proof-stepwise
@@ -1250,7 +1241,8 @@ should match the `coq-show-proof-diffs-regexp'."
(> (length coq-last-but-one-proofstack) 0)))
(coq--show-proof-stepwise-cmds))))
-
+;; This does not Set Printing Width, it rather tells pg to do that before each
+;; command (if necessary)
(defpacustom auto-adapt-printing-width t
"If non-nil, adapt automatically printing width of goals window.
Each time the user sends a bunch of commands to Coq, check if the
@@ -1260,17 +1252,7 @@ is chosen arbitrarily. WARNING 2: when backtracking the
printing
width is synchronized by coq (?!)."
:type 'boolean
:safe 'booleanp
- :group 'coq
- :eval (coq-set-auto-adapt-printing-width))
-
-
-;; defpacustom fails to call :eval during inititialization, see trac #456
-(coq-set-auto-adapt-printing-width)
-
-;; this initiates auto 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 t)
+ :group 'coq)
(defvar coq-shell-current-line-width nil
"Current line width of the Coq printing width.
@@ -1333,14 +1315,15 @@ present, current pg display mode and current geometry
otherwise."
A Show command is also issued if SHOW is non-nil, so that the goal is
redisplayed."
(interactive)
- (let ((wdth (or width (coq-guess-goal-buffer-at-next-command))))
- ;; if no available width, or unchanged, do nothing
- (when (and wdth (not (equal wdth coq-shell-current-line-width)))
- (proof-shell-invisible-command (format "Set Printing Width %S." (- wdth
1)) t)
- (setq coq-shell-current-line-width wdth)
- ;; Show iff show non nil and some proof is under way
- (when (and show (not (null (cl-caddr (coq-last-prompt-info-safe)))))
- (proof-shell-invisible-command (format "Show.") t nil
'no-error-display)))))
+ (when coq-auto-adapt-printing-width
+ (let ((wdth (or width (coq-guess-goal-buffer-at-next-command))))
+ ;; if no available width, or unchanged, do nothing
+ (when (and wdth (not (equal wdth coq-shell-current-line-width)))
+ (proof-shell-invisible-command (format "Set Printing Width %S." (-
wdth 1)) t)
+ (setq coq-shell-current-line-width wdth)
+ ;; Show iff show non nil and some proof is under way
+ (when (and show (not (null (cl-caddr (coq-last-prompt-info-safe)))))
+ (proof-shell-invisible-command (format "Show.") t nil
'no-error-display))))))
(defun coq-adapt-printing-width-and-show (&optional _show width)
(interactive)
