Various cosmetic changes and fix some warnings

Enable `lexical-binding` when missing in the files recently modified.
Fix compile warnings about quotes in docstrings.
Prefer #' to quote function names.

* coq/coq.el: Require `proof-syntax`, `proof-useropts`, and
`proof-utils` to silence some compiler warnings.
(action, string): Move dynbound declaration to a smaller scope in
`coq-preprocessing`.
(coq-set-state-infos, coq-grab-punctuation-left): Fit docstring within
80 columns.
(coq-diffs--setter, coq-diffs): Move `coq-diffs` var before first use.
(coq-shell-theorem-dependency-list-regexp)
(coq-dependency-menu-system-specific)
(coq-dependencies-system-specific): Move vars before their first use.
(coq-proof-tree-insert-evar-command): Simplify with `or`.
(coq-preprocessing): Declare `action` and `string` locally to be dynbound.
(coq-highlight-span-dependencies): Remove unused var `proof-pos`.
<trailer>: Remove second coding cookie since .el files default to utf-8.

* generic/pg-autotest.el: Use `lexical-binding`.
(pg-autotest-test-script-randomjumps): Remove unused var `random-edit`.
(pg-autotest-test-eval): Use lexical binding.

* generic/proof-script.el (proof-colour-locked, proof-setup-imenu)
(proof-colour-locked-span, proof-script-delete-spans)
(proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window):
Fit docstring within 80 columns.

* generic/proof-syntax.el: Use `lexical-binding`.
(proof-replace-regexp-in-string, proof-re-search-forward)
(proof-re-search-backward, proof-re-search-forward-safe):
Fit docstring within 80 columns.
(proof-format): Use lexical binding.

* doc/PG-adapting.texi: (Auto)Update accordingly.

Author: monnier

coq/coq.el

@@ -32,15 +32,17 @@
 (require 'cl-lib)
 
 (require 'span)
+(require 'proof-syntax)
+(require 'proof-useropts)
+(require 'proof-utils)
 (eval-when-compile
   (require 'proof-utils)
   (require 'span)
   (require 'outline)
   (require 'newcomment)
   (require 'etags))
+
 (defvar proof-info)       ; dynamic scope in proof-tree-urgent-action
-(defvar action)       ; dynamic scope in coq-insert-as stuff
-(defvar string)       ; dynamic scope in coq-insert-as stuff
 (defvar old-proof-marker)
 (defvar coq-keymap)
 (defvar coq-one-command-per-line)
@@ -177,7 +179,7 @@ It is mostly useful in three window mode, see also
 `proof-three-window-mode-policy' for details."
 
   :type 'boolean
-  :safe 'booleanp
+  :safe #'booleanp
   :group 'coq-auto-compile)
 
 ;;
@@ -591,11 +593,11 @@ and read by function `coq-empty-action-list-command'.")
   (span-set-property span 'statenum val))
 
 (defsubst coq-get-span-goalcmd (span)
-  "Return the 'goalcmd flag of the SPAN."
+  "Return the `goalcmd' flag of the SPAN."
   (span-property span 'goalcmd))
 
 (defsubst coq-set-span-goalcmd (span val)
-  "Set the 'goalcmd flag of the SPAN to VAL."
+  "Set the `goalcmd' flag of the SPAN to VAL."
   (span-set-property span 'goalcmd val))
 
 (defsubst coq-set-span-proofnum (span val)
@@ -625,7 +627,7 @@ and read by function `coq-empty-action-list-command'.")
 
 (defun coq-set-state-infos ()
   "Set the last locked span's state number to the number found last time.
-This number is in the *last but one* prompt (variable `coq-last-but-one-statenum').
+This number is in the *last but one* prompt (var `coq-last-but-one-statenum').
 If locked span already has a state number, then do nothing. Also updates
 `coq-last-but-one-statenum' to the last state number for next time."
   (if proof-shell-last-prompt
@@ -815,7 +817,7 @@ If C is nil, return nil."
     (or (equal (char-syntax c) ?\.) (equal (char-syntax c) ?\_))))
 
 (defun coq-grab-punctuation-left (pos)
-  "Return a string made of punctuations chars found immediately before position POS."
+  "Return the punctuation chars found immediately before position POS."
   (let ((res nil)
         (currpos pos))
     (while (coq-is-symbol-or-punct (char-before currpos))
@@ -931,7 +933,7 @@ Otherwise propose identifier at point if any."
 
 (defun coq-command-with-set-unset (setcmd cmd unsetcmd &optional postformatcmd testcmd)
   "Play commands SETCMD then CMD and then silently UNSETCMD.
-The last UNSETCMD is performed with tag 'empty-action-list so that it
+The last UNSETCMD is performed with tag `empty-action-list' so that it
 does not trigger ‘proof-shell-empty-action’ (which does \"Show\" at
 the time of writing this documentation)."
   (let* ((postform (if (eq postformatcmd nil) 'identity postformatcmd))
@@ -1119,7 +1121,7 @@ With flag Printing All if some prefix arg is given (C-u)."
   (coq-ask-do-show-all "Check" "Check"))
 
 (defun coq-get-response-string-at (&optional pt)
-  "Go forward from PT until reaching a 'response property, and return it.
+  "Go forward from PT until reaching a `response' property, and return it.
 Response span only starts at first non space character of a
 command, so we may have to go forward to find it.  Starts
 from (point) if pt is nil.  Precondition: pt (or point if nil)
@@ -1183,6 +1185,27 @@ Printing All set."
 (add-hook 'proof-assert-command-hook #'coq-adapt-printing-width)
 (add-hook 'proof-retract-command-hook #'coq-reset-printing-width)
 
+(defun coq-diffs--setter (symbol new-value)
+  ":set function fo `coq-diffs'.
+Set Diffs setting if Coq is running and has a version >= 8.10."
+  (set symbol new-value)
+  (if (proof-shell-available-p)
+      (let ((cmd (coq-diffs)))
+        (if (equal cmd "")
+            (message "Ignore coq-diffs setting %s for Coq before 8.10"
+                 (symbol-name coq-diffs))
+          (proof-shell-invisible-command cmd)))))
+
+(defcustom coq-diffs 'off
+  "Controls Coq Diffs option"
+  :type '(radio
+    (const :tag "Don't show diffs" off)
+    (const :tag "Show diffs: only added" on)
+    (const :tag "Show diffs: added and removed" removed))
+  :safe (lambda (v) (member v '(off on removed)))
+  :set #'coq-diffs--setter
+  :group 'coq)
+
 (defun coq--show-proof-stepwise-cmds ()
   (when coq-show-proof-stepwise
     (if (coq--post-v811)
@@ -1202,7 +1225,7 @@ Printing All set."
 (defun coq-empty-action-list-command (cmd)
   "Return the list of commands to send to Coq after CMD
 if it is the last command of the action list.
-If CMD is tagged with 'empty-action-list then this function won't
+If CMD is tagged with `empty-action-list' then this function won't
 be called and no command will be sent to Coq.
 Note: the last command added if `coq-show-proof-stepwise' is set
 should match the `coq-show-proof-diffs-regexp'."
@@ -1959,6 +1982,41 @@ at `proof-assistant-settings-cmds' evaluation time.")
   (proof-config-done)
   )
 
+;; This variable is used by generic pg code. Every time this is detected in the
+;; output, it sets the `proof-last-theorem-dependencies' variable. Substring 1
+;; should contain the name of the theorem, and substring 2 should contain its
+;; dependencies. The content of `proof-last-theorem-dependencies' is then used
+;; by pg generic code to trigger `proof-depends-process-dependencies', which
+;; itself sets the 'dependencies property of the span, and calls
+;; `proof-dependencies-system-specific'. The latter is bound to
+;; `coq-dependencies-system-specific' below.
+(defconst coq-shell-theorem-dependency-list-regexp
+  "<infomsg>\n?The proof of \\(?1:[^ \n]+\\)\\(?: \\|\n\\)should start with one of the following commands:\\(?: \\|\n\\)Proof using\\(?2:[^.]*\\)\\.")
+
+
+;; the additional menu for "proof using". highlights the "Proof." command, and
+;; have a entry to insert the annotation and remove the highlight.
+(defvar coq-dependency-menu-system-specific
+  (lambda (span)
+    (let* ((deps (span-property-safe span 'dependencies))
+           (specialspans (spans-at-region-prop (span-start span) (span-end span) 'proofusing))
+           (specialspan (and specialspans (not (cdr specialspans)) (car specialspans)))
+           (suggested (mapconcat #'identity deps " "))
+           (suggested (coq-hack-proofusing-suggestion suggested))
+           (name (concat " insert \"proof using " suggested "\""))
+           (fn (lambda (sp)
+                 (coq-insert-proof-using-suggestion sp t)
+                 (and specialspan (span-delete specialspan)))))
+      (list "-------------" (vector name `(,fn ,span) t))))
+  "Coq specific additional menu entry for \"Proof using\".
+annotation. See `proof-dependency-menu-system-specific'." )
+
+(defvar coq-dependencies-system-specific
+  (lambda (span)
+    (coq-insert-proof-using-suggestion span))
+  "Coq specific dependency mechanism.
+Used for automatic insertion of \"Proof using\" annotations.")
+
 (defun coq-shell-mode-config ()
   (setq
    proof-shell-cd-cmd coq-shell-cd
@@ -2113,27 +2171,6 @@ Return the empty string if the version of Coq < 8.10."
       (format "Set Diffs \"%s\". " (symbol-name coq-diffs))
     ""))
 
-(defun coq-diffs--setter (symbol new-value)
-  ":set function fo `coq-diffs'.
-Set Diffs setting if Coq is running and has a version >= 8.10."
-  (set symbol new-value)
-  (if (proof-shell-available-p)
-      (let ((cmd (coq-diffs)))
-        (if (equal cmd "")
-            (message "Ignore coq-diffs setting %s for Coq before 8.10"
-                 (symbol-name coq-diffs))
-          (proof-shell-invisible-command cmd)))))
-
-(defcustom coq-diffs 'off
-  "Controls Coq Diffs option"
-  :type '(radio
-    (const :tag "Don't show diffs" off)
-    (const :tag "Show diffs: only added" on)
-    (const :tag "Show diffs: added and removed" removed))
-  :safe (lambda (v) (member v '(off on removed)))
-  :set #'coq-diffs--setter
-  :group 'coq)
-
 ;; Obsolete:
 ;;(defpacustom undo-depth coq-default-undo-limit
 ;;  "Depth of undo history.  Undo behaviour will break beyond this size."
@@ -2217,7 +2254,7 @@ Show commands before the next real proof command.
 The ID's of the open goals are checked with
 `proof-tree-sequent-hash' in order to find out if they are new.
 For any new goal an appropriate Show Goal command with a
-'proof-tree-show-subgoal flag is inserted into
+`proof-tree-show-subgoal' flag is inserted into
 `proof-action-list'.  Then, in the normal delayed output
 processing, the sequent text is send to prooftree as a sequent
 update (see `proof-tree-update-sequent') and the ID of the
@@ -2336,7 +2373,7 @@ fact in `coq--proof-tree-must-disable-evars'."
   "Insert an evar printing command at the head of `proof-action-list'."
   (push (proof-shell-action-list-item
          (concat cmd " Printing Dependent Evars Line.")
-         (if callback callback 'proof-done-invisible)
+         (or callback #'proof-done-invisible)
          (list 'invisible))
         proof-action-list))
 
@@ -2406,8 +2443,10 @@ result of `coq-proof-tree-get-proof-info'."
 (defun coq-bullet-p (s)
   (string-match coq-bullet-regexp-nospace s))
 
-;; Remark: `action' and `string' are known by `proof-shell-insert-hook'
 (defun coq-preprocessing ()
+  ;; Remark: `action' and `string' are known by `proof-shell-insert-hook'
+  (defvar action)       ; dynamic scope in coq-insert-as stuff
+  (defvar string)       ; dynamic scope in coq-insert-as stuff
   (when coq-time-commands
     (with-no-warnings  ;; NB: dynamic scoping of `string' and `action'
       ;; Don't add the prefix if this is a command sent internally
@@ -2620,17 +2659,6 @@ Warning: this makes the error messages (and location) wrong.")
 ;; already performed.).
 
 
-;; This variable is used by generic pg code. Every time this is detected in the
-;; output, it sets the `proof-last-theorem-dependencies' variable. Substring 1
-;; should contain the name of the theorem, and substring 2 should contain its
-;; dependencies. The content of `proof-last-theorem-dependencies' is then used
-;; by pg generic code to trigger `proof-depends-process-dependencies', which
-;; itself sets the 'dependencies property of the span, and calls
-;; `proof-dependencies-system-specific'. The latter is bound to
-;; `coq-dependencies-system-specific' below.
-(defconst coq-shell-theorem-dependency-list-regexp
-  "<infomsg>\n?The proof of \\(?1:[^ \n]+\\)\\(?: \\|\n\\)should start with one of the following commands:\\(?: \\|\n\\)Proof using\\(?2:[^.]*\\)\\.")
-
 (defcustom coq-accept-proof-using-suggestion 'highlight
   "Whether and how proofgeneral should insert \"Proof using\" suggestions.
 Suggestions are emitted by Coq at Qed time. The possible values
@@ -2674,23 +2702,6 @@ Remarks and limitations:
 (defun coq-hack-proofusing-suggestion (suggested)
   (if (string-equal "" suggested) "Type" suggested))
 
-;; the additional menu for "proof using". highlights the "Proof." command, and
-;; have a entry to insert the annotation and remove the highlight.
-(defvar coq-dependency-menu-system-specific
-  (lambda (span)
-    (let* ((deps (span-property-safe span 'dependencies))
-           (specialspans (spans-at-region-prop (span-start span) (span-end span) 'proofusing))
-           (specialspan (and specialspans (not (cdr specialspans)) (car specialspans)))
-           (suggested (mapconcat #'identity deps " "))
-           (suggested (coq-hack-proofusing-suggestion suggested))
-           (name (concat " insert \"proof using " suggested "\""))
-           (fn (lambda (sp)
-                 (coq-insert-proof-using-suggestion sp t)
-                 (and specialspan (span-delete specialspan)))))
-      (list "-------------" (vector name `(,fn ,span) t))))
-  "Coq specific additional menu entry for \"Proof using\".
-annotation. See `proof-dependency-menu-system-specific'." )
-
 (defconst coq-proof-using-regexp "\\_<Proof\\(?1:[^.]*\\)\\."
   "Regexp matching Coq \"Proof ....\" annotation (with no \"using\" annotation).
 We suppose there is no \"using\" annotation, since Coq will fail
@@ -2706,7 +2717,7 @@ insertion point for the \"using\" annotation. ")
 (defun coq-highlight-span-dependencies (start end _suggested)
   (goto-char start)
   ; Search for the "Proof" command and build a hilighted span on it
-  (let* ((proof-pos (match-beginning 0))
+  (let* (;; (proof-pos (match-beginning 0))
          (newspan (span-make start end)))
     (span-set-property newspan 'face 'proof-warning-face)
     (span-set-property newspan 'help-echo "Right click to insert \"proof using\"")
@@ -2783,12 +2794,6 @@ SPAN is the span of the whole theorem (statement + proof)."
                   (coq-highlight-span-dependencies proof-pos proof-end string-suggested)
                   (message "\"Proof using\" not set. M-x coq-insert-suggested-dependency or right click to add it. See also `coq-accept-proof-using-suggestion'."))))))))))
 
-(defvar coq-dependencies-system-specific
-  (lambda (span)
-    (coq-insert-proof-using-suggestion span))
-  "Coq specific dependency mechanism.
-Used for automatic insertion of \"Proof using\" annotations.")
-
 
 (defun coq-insert-as-in-next-command ()
   (interactive)
@@ -3483,7 +3488,6 @@ coq from the new opam switch."
 ;;   Local Variables: ***
 ;;   fill-column: 79 ***
 ;;   indent-tabs-mode: nil ***
-;;   coding: utf-8 ***
 ;;   End: ***
 
 ;;; coq.el ends here

doc/PG-adapting.texi

@@ -788,7 +788,7 @@ override this with a system-specific function.
 @c TEXI DOCSTRING MAGIC: proof-looking-at-syntactic-context
 @defun proof-looking-at-syntactic-context 
 Determine if current point is at beginning or within comment/string context.@*
-If so, return a symbol indicating this ('comment or @code{'string}).
+If so, return a symbol indicating this (@samp{comment} or @samp{string}).
 This function invokes <PA-syntactic-context> if that is defined, otherwise
 it calls @samp{@code{proof-looking-at-syntactic-context}}.
 @end defun
@@ -3665,7 +3665,7 @@ user option @samp{@code{proof-auto-action-when-deactivating-scripting}}.
 If @samp{@code{proof-no-fully-processed-buffer}} is t there is only the choice
 to fully retract the active scripting buffer.  In this case the
 active scripting buffer is retracted even if it was fully processed.
-Setting @samp{@code{proof-auto-action-when-deactivating-scripting}} to @code{'process}
+Setting @samp{@code{proof-auto-action-when-deactivating-scripting}} to @samp{process}
 is ignored in this case.
 
 If the scripting buffer is (or has become) fully processed, and it is

generic/pg-autotest.el

@@ -1,4 +1,4 @@
-;;; pg-autotest.el --- Simple testing framework for Proof General
+;;; pg-autotest.el --- Simple testing framework for Proof General  -*- lexical-binding: t; -*-
 
 ;; This file is part of Proof General.
 
@@ -39,7 +39,7 @@
   "Flag indicating overall successful state of tests.")
 
 (defvar pg-autotest-log t
-  "Value for 'standard-output' during tests.")
+  "Value for `standard-output' during tests.")
 
 ;;; Some utilities
 
@@ -106,7 +106,7 @@
 
 (defun pg-autotest-message (msg &rest args)
   "Give message MSG (formatted using ARGS) in log file output and on display."
-  (let ((fmsg   (if args (apply 'format msg args) msg)))
+  (let ((fmsg   (if args (apply #'format msg args) msg)))
     (proof-with-current-buffer-if-exists
      pg-autotest-log
      (insert fmsg "\n"))
@@ -117,7 +117,7 @@
   (pg-autotest-message "\n\nREMARK: %s\n" msg))
 
 (defun pg-autotest-timestart (&optional clockname)
-  "Make a note of current time, named 'local or CLOCKNAME."
+  "Make a note of current time, named `local' or CLOCKNAME."
   (put 'pg-autotest-time (or clockname 'local)
        (current-time)))
 
@@ -208,7 +208,7 @@ completely processing the buffer as the last step."
   (pg-autotest-find-file-restart file)
   (while (> jumps 0)
     (let* ((random-point     (random (point-max)))
-	   (random-edit      nil) ; (< 20 (random 100)))
+	   ;; (random-edit      nil) ; (< 20 (random 100)))
 	   (random-thing     (random 10)))
       (cond
        ((and (eq random-thing 0)
@@ -277,7 +277,7 @@ completely processing the buffer as the last step."
 
 (defun pg-autotest-test-eval (body)
   "Evaluate given expression for side effect."
-  (eval body))
+  (eval body t))
 
 (defun pg-autotest-test-quit-prover ()
   "Exit prover process."