branch: scratch/proof-general
commit 08189b7f3879f1f3558b8a9d6ce91902358e9bf0
Author: Stefan Monnier <[email protected]>
Commit: Stefan Monnier <[email protected]>
pg-user.el: Misc cleanups from compilation warnings
* generic/pg-user.el: Fix docstring markup warnings.
Avoid `point-at-eol`, declared obsolete in Emacs-29.
Prefer #' to quote function names.
(proof-electric-terminator-enable): Add FIXMEs.
(proof-check-annotate-source): Pass 2nd arg to `looking-back` to try
and avoid pathological behaviors (and silence a warning).
(proof-check-generate-report): Add FIXME about use of `coq-*` variable
in this generic files.
(proof-autosend-loop-all, proof-autosend-loop-next):
Remove `unwind-protect` used without any unwind form.
---
generic/pg-user.el | 153 +++++++++++++++++++++++++++--------------------------
1 file changed, 77 insertions(+), 76 deletions(-)
diff --git a/generic/pg-user.el b/generic/pg-user.el
index e7a088d551..88d5026d63 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -532,8 +532,10 @@ This is intended as a value for
`proof-activate-scripting-hook'"
;;;###autoload
(defun proof-electric-terminator-enable (&optional arg)
+ ;; FIXME: This should be defined using `define-minor-mode'.
+ ;; FIXME: I can't see where `proof-set-value' is involved!
"Ensure modeline update to display new value for electric terminator.
-This a function is called by the custom-set property 'proof-set-value.
+This function is called by the custom-set property `proof-set-value'.
It can also be used as a minor mode function: with ARG, turn on iff ARG>0"
(unless (null arg)
(setq proof-electric-terminator-enable (> (prefix-numeric-value arg) 0)))
@@ -638,7 +640,8 @@ white space."
;; to the start of the command.
(re-search-forward "[[:blank:]\n]*")
(end-of-line)
- (when (looking-back "(\\* \\(PASS\\|FAIL\\) \\*)")
+ (when (looking-back "(\\* \\(PASS\\|FAIL\\) \\*)"
+ (line-beginning-position))
(delete-char -10)
(delete-horizontal-space))
(when (or annotate-passing (not (car pr)))
@@ -671,6 +674,7 @@ the results to the file denoted by BATCH."
;; determine a relative file name for current buffer
(when buffer-file-name
+ ;; FIXME: `coq-project-filename'? Isn't this supposed to be generic code?
(setq coq-proj-dir (locate-dominating-file buffer-file-name
coq-project-filename)))
(if coq-proj-dir
@@ -726,14 +730,14 @@ CHUNKS must be the reversed result of
`proof-script-omit-filter'
for a whole buffer. (Only the top-level must be reversed, the
commands inside the chunks must be as returned by
`proof-script-omit-filter', that is in reversed order.) CHUNKS
-must not contain any 'nested-proof chunk.
+must not contain any `nested-proof' chunk.
This function processes the content of CHUNKS normally by
-asserting them one by one. Any error reported inside a 'no-proof
-chunk is reported as error to the user. 'proof chunks containing
+asserting them one by one. Any error reported inside a `no-proof'
+chunk is reported as error to the user. `proof' chunks containing
errors are silently replaced by
`proof-script-proof-admit-command'. The result is a list of proof
-status results, one for each 'proof chunk in the same order. Each
+status results, one for each `proof' chunk in the same order. Each
proof-status result is a list of 4 elements as follows.
- 1st: proof status as `t' or `nil'. Proofs closed with a match
of `proof-omit-cheating-regexp', if defined, count as failing,
@@ -742,12 +746,12 @@ proof-status result is a list of 4 elements as follows.
`proof-get-proof-info-fn'.
- 3rd: Position of the start of the span containing the theorem
to prove. More precisely, it is the second last span of the
- 'no-proof chunk before the 'proof chunk. Note that spans
+ `no-proof' chunk before the `proof' chunk. Note that spans
usually contain preceeding white space. Therefore this position
is not necessarily the first letter of the keyword introducing
the theorem statement.
- 4rd: Position of the start of the span containing \"Proof
- using\". More precisely, it is the last span in the 'no-proof
+ using\". More precisely, it is the last span in the `no-proof'
chunk before the proof."
(let (proof-results current-proof-state-and-name proof-start-points)
(while chunks
@@ -900,7 +904,7 @@ is reported to the user without generating an overview. The
overview only contains those names of theorems whose proof
scripts are classified as opaque by the omit-proofs feature. For
Coq for instance, among others, proof scripts terminated with
-'Defined' are not opaque and do not appear in the generated
+\"Defined\" are not opaque and do not appear in the generated
overview.
Note that this command does not (re-)compile required files.
@@ -1375,12 +1379,12 @@ If called interactively, ARG is given by the prefix
argument."
(goto-char unproc)
(skip-chars-forward " \t\n")
(point)))
- (end (point-at-eol)))
+ (end (line-end-position)))
(cond
((< start end)
(delete-region start end))
- ((< start (point-at-eol))
- (delete-region start (point-at-eol))))))
+ ((< start (line-end-position))
+ (delete-region start (line-end-position))))))
(defun pg-get-old-input ()
"Return text between end of locked region and point, up to EOL.
@@ -1390,7 +1394,7 @@ If there is no text, return the empty string."
(goto-char unproc)
(skip-chars-forward " \t\n")
(point)))
- (end (point-at-eol)))
+ (end (line-end-position)))
(if (< start end)
(buffer-substring-no-properties start end)
nil)))
@@ -1572,8 +1576,8 @@ removed if it matches the last item in the ring."
;; functions `pg-protected-undo-1' and `pg--next-undo-delta'
;;
-(define-key proof-mode-map [remap undo] 'pg-protected-undo)
-(define-key proof-mode-map [remap advertised-undo] 'pg-protected-undo)
+(define-key proof-mode-map [remap undo] #'pg-protected-undo)
+(define-key proof-mode-map [remap advertised-undo] #'pg-protected-undo)
(defun pg-protected-undo (&optional arg)
"As `undo' but avoids breaking the locked region.
@@ -1680,7 +1684,7 @@ Assume the `undo-in-region' behavior will apply if ARG is
non-nil."
(defvar proof-autosend-timer nil "Timer used by autosend.")
(deflocal proof-autosend-modified-tick nil
- "Records 'buffer-chars-modified-tick' since last autosend.")
+ "Records `buffer-chars-modified-tick' since last autosend.")
;;;###autoload
(defun proof-autosend-enable (&optional nomsg)
@@ -1690,7 +1694,7 @@ Assume the `undo-in-region' behavior will apply if ARG is
non-nil."
(when proof-autosend-enable
(setq proof-autosend-timer
(run-with-idle-timer proof-autosend-delay
- t 'proof-autosend-loop))
+ t #'proof-autosend-loop))
(setq proof-autosend-modified-tick nil)
(unless nomsg (message "Automatic sending turned on.")))
(when (not proof-autosend-enable)
@@ -1718,68 +1722,65 @@ Assume the `undo-in-region' behavior will apply if ARG
is non-nil."
(defun proof-autosend-loop-all ()
"Send commands from the script until an error, complete, or input appears."
(message "Sending commands to prover...")
- (unwind-protect
- (progn
- (save-excursion
- (goto-char (point-max))
- (proof-assert-until-point
- (if proof-multiple-frames-enable
- 'no-minibuffer-messages ; nb: not API
- '(no-response-display
- no-error-display
- no-goals-display))))
- (proof-shell-wait t) ; interruptible
- (cond
- ((eq proof-shell-last-output-kind 'error)
- (message "Sending commands to prover...error"))
- ((and (input-pending-p) proof-shell-busy)
- (proof-interrupt-process)
- (message "Sending commands to prover...interrupted")
- (proof-shell-wait))
- (t
- (message "Sending commands to prover...done"))))))
+ (save-excursion
+ (goto-char (point-max))
+ (proof-assert-until-point
+ (if proof-multiple-frames-enable
+ 'no-minibuffer-messages ; nb: not API
+ '(no-response-display
+ no-error-display
+ no-goals-display))))
+ (proof-shell-wait t) ; interruptible
+ (cond
+ ((eq proof-shell-last-output-kind 'error)
+ (message "Sending commands to prover...error"))
+ ((and (input-pending-p) proof-shell-busy)
+ (proof-interrupt-process)
+ (message "Sending commands to prover...interrupted")
+ (proof-shell-wait))
+ (t
+ (message "Sending commands to prover...done"))))
(defun proof-autosend-loop-next ()
"Send the next command from the script and indicate its success/otherwise."
- (unwind-protect
- (let ((qol (proof-queue-or-locked-end)))
- (save-excursion
- ;(goto-char qol)
- ;(skip-chars-forward " \t\n")
- (message "Trying next commands in prover...")
- (proof-assert-until-point
- (if proof-multiple-frames-enable
- 'no-minibuffer-messages ; nb: not API
- '(no-response-display
- no-error-display
- no-goals-display))))
- (let ((proof-sticky-errors t))
- (proof-shell-wait t)) ; interruptible
- (cond
- ((eq proof-shell-last-output-kind 'error)
- (message "Trying next commands in prover...error"))
- ((and (input-pending-p) proof-shell-busy)
- (proof-interrupt-process)
- (message "Trying next commands in prover...interrupted")
- (proof-shell-wait))
- (t
- (message "Trying next commands in prover...OK")))
- ;; success: now undo in prover, highlight undone spans if OK
- (unless (eq qol (proof-queue-or-locked-end)) ; no progress
- (save-excursion
- (goto-char qol)
- (proof-retract-until-point
- (lambda (beg end)
- (span-make-self-removing-span
- (save-excursion
- (goto-char beg)
- (skip-chars-forward " \t\n")
- (point))
- end
- 'face 'highlight))
- '(no-response-display
- no-error-display
- no-goals-display)))))))
+ (let ((qol (proof-queue-or-locked-end)))
+ (save-excursion
+ ;;(goto-char qol)
+ ;;(skip-chars-forward " \t\n")
+ (message "Trying next commands in prover...")
+ (proof-assert-until-point
+ (if proof-multiple-frames-enable
+ 'no-minibuffer-messages ; nb: not API
+ '(no-response-display
+ no-error-display
+ no-goals-display))))
+ (let ((proof-sticky-errors t))
+ (proof-shell-wait t)) ; interruptible
+ (cond
+ ((eq proof-shell-last-output-kind 'error)
+ (message "Trying next commands in prover...error"))
+ ((and (input-pending-p) proof-shell-busy)
+ (proof-interrupt-process)
+ (message "Trying next commands in prover...interrupted")
+ (proof-shell-wait))
+ (t
+ (message "Trying next commands in prover...OK")))
+ ;; success: now undo in prover, highlight undone spans if OK
+ (unless (eq qol (proof-queue-or-locked-end)) ; no progress
+ (save-excursion
+ (goto-char qol)
+ (proof-retract-until-point
+ (lambda (beg end)
+ (span-make-self-removing-span
+ (save-excursion
+ (goto-char beg)
+ (skip-chars-forward " \t\n")
+ (point))
+ end
+ 'face 'highlight))
+ '(no-response-display
+ no-error-display
+ no-goals-display))))))
(provide 'pg-user)
