Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev.

Fix a few more cl.el leftovers.  Get rid of remaining use of iso-2022.
Use SMIE unconditionally.

* coq/coq-abbrev.el: Use lexical-binding.
(coq-install-abbrevs): Delete, only keep the relevant contents.
(proof-defstringset-fn): Remove.  Fold changes into the main version.

* coq/coq-indent.el (coq-find-real-start): Use forward-comment.

* coq/coq-smie.el: Use lexical-binding.  Assume `smie` is available.
(coq--string-suffix-p): Rename from coq-string-suffix-p.
Use string-suffix-p for it when available.
(string-suffix-p): Never define here.  Change all users to use
coq--string-suffix-p instead.
(coq-smie-.-deambiguate): Use forward-comment.  Remove unused var `beg`.
(coq-backward-token-fast-nogluing-dot-friends)
(coq-forward-token-fast-nogluing-dot-friends): Remove unused var
`tok-other`.
(coq-smie-search-token-backward): Remove unused var `p`.
(coq-smie-:=-deambiguate, coq-smie-backward-token): Prefer char-before
over looking-back.
(coq-smie-rules): Use `pcase` over deprecated cl's `case`.

* coq/coq-syntax.el: Use lexical-binding.
(coq-count-match): Rewrite so it doesn't do needless heap-allocation.
(coq-module-opening-p, coq-section-command-p, coq-goal-command-str-p):
Use case-fold-search rather than proof-string-match.
(coq-goal-command-regexp): Forward-declare.
(coq-save-command-regexp-strict): Move before first use.
(coq-reserved-regexp): Use a single \_< ... \_>.
(coq-detect-hyps-positions): Limit search for looking-back.

* coq/coq.el: Remove SMIE declarations since SMIE is always used.
(coq-use-smie): Remove, unused.
(coq-smie): Always require.

* generic/pg-pbrpm.el: Fix leftover cl.el uses.

* generic/proof-utils.el (proof-defstringset-fn): Fix copy&paste error
in the docstring, improve interactive prompt.

* lib/maths-menu.el: Use utf-8 and lexical-binding.

1 files changed, 35 insertions, 29 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index e1a9a7e3..7a11a43f 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1,4 +1,4 @@
-;;; coq-syntax.el --- Font lock expressions for Coq
+;;; coq-syntax.el --- Font lock expressions for Coq  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -987,14 +987,15 @@ so for the following reasons:
 ;;      elle declare un module.
 ;;    (la fonction vernac_declare_module dans toplevel/vernacentries)
 
-(defun coq-count-match (regexp strg)
-  "Count the number of max. non-overlapping substring of STRG matching REGEXP.
+(defun coq-count-match (regexp str)
+  "Count the number of max. non-overlapping substring of STR matching REGEXP.
 Empty matches are counted once."
-  (let ((nbmatch 0) (str strg))
-    (while (and (proof-string-match regexp str) (not (string-equal str "")))
+  (let ((nbmatch 0) (pos 0) (end (length str))
+        (case-fold-search nil))
+    (while (and (< pos end)
+                (string-match regexp str pos))
       (cl-incf nbmatch)
-      (if (= (match-end 0) 0) (setq str (substring str 1))
-        (setq str (substring str (match-end 0)))))
+      (setq pos (max (match-end 0) (1+ pos))))
     nbmatch))
 
 ;; Module and or section openings are detected syntactically. Module
@@ -1009,12 +1010,16 @@ Used by `coq-goal-command-p'"
   (let* ((match (coq-count-match "\\_<match\\_>" str))
          (with (coq-count-match "\\_<with\\_>" str))
          (letwith (+ (coq-count-match "\\_<let\\_>" str) (- with match)))
-         (affect (coq-count-match ":=" str)))
-    (and (proof-string-match "\\`\\(Module\\)\\_>" str)
+         (affect (coq-count-match ":=" str))
+         (case-fold-search nil))
+    (and (string-match "\\`\\(Module\\)\\_>" str)
          (= letwith affect))))
 
 (defun coq-section-command-p (str)
-  (proof-string-match "\\`\\(Section\\|Chapter\\)\\_>" str))
+  (let ((case-fold-search nil))
+    (string-match "\\`\\(Section\\|Chapter\\)\\_>" str)))
+
+(defvar coq-goal-command-regexp)
 
 ;; unused anymore (for good)
 (defun coq-goal-command-str-p (str)
@@ -1023,16 +1028,17 @@ Use ‘coq-goal-command-p’ on a span instead if possible."
   (let* ((match (coq-count-match "\\_<match\\_>" str))
          (with (- (coq-count-match "\\_<with\\_>" str) (coq-count-match "\\_<with\\s-+signature\\_>" str)))
          (letwith (+ (coq-count-match "\\_<let\\_>" str) (- with match)))
-         (affect (coq-count-match ":=" str)))
-    (and (proof-string-match coq-goal-command-regexp str)
+         (affect (coq-count-match ":=" str))
+         (case-fold-search nil))
+    (and (string-match coq-goal-command-regexp str)
          (not
           (and
-           (proof-string-match
+           (string-match
             (concat "\\`\\(Local\\|Definition\\|Lemma\\|Theorem\\|Fact\\|Add\\|Let\\|Program\\|Module\\|Class\\|Instance\\)\\_>")
             str)
            (not (= letwith affect))))
-         (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:"
-                                  str)))))
+         (not (string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:"
+                            str)))))
 
 ;; This is the function that tests if a SPAN is a goal start. All it
 ;; has to do is look at the 'goalcmd attribute of the span.
@@ -1063,8 +1069,15 @@ It is used:
   (append coq-keywords-save-strict '("Proof"))
   )
 
+;; According to Coq, "Definition" is both a declaration and a goal.
+;; It is understood here as being a goal.  This is important for
+;; recognizing global identifiers, see coq-global-p.
+(defconst coq-save-command-regexp-strict
+  (proof-anchor-regexp
+   (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict)
+           "\\)")))
 
-(defun coq-save-command-p (span str)
+(defun coq-save-command-p (_span str)
   "Decide whether argument is a Save command or not."
   (or (proof-string-match coq-save-command-regexp-strict str)
       (and (proof-string-match "\\`Proof\\_>" str)
@@ -1151,8 +1164,10 @@ It is used:
 ;; FIXME: actually these are not exactly reserved keywords, find
 ;; another classification of keywords.
 (defvar coq-reserved-regexp
-  (concat "\\_<with\\s-+signature\\_>\\|"
-   (proof-ids-to-regexp coq-reserved)))
+  (concat "\\_<"
+          "\\(?:with\\s-+signature\\|"
+          (regexp-opt coq-reserved) "\\)"
+          "\\_>"))
 
 (defvar coq-state-changing-tactics
   (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing))
@@ -1276,16 +1291,6 @@ It is used:
   "*Font-lock table for Coq terms.")
 
 
-
-;; According to Coq, "Definition" is both a declaration and a goal.
-;; It is understood here as being a goal.  This is important for
-;; recognizing global identifiers, see coq-global-p.
-(defconst coq-save-command-regexp-strict
-  (proof-anchor-regexp
-   (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict)
-           "\\)")))
-
-
 (defconst coq-save-command-regexp
   (proof-anchor-regexp
    (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save)
@@ -1402,7 +1407,8 @@ part of another hypothesis.")
                         (search-forward-regexp coq-hyp-name-or-goalsep-in-goal-or-response-regexp nil t)
                         (goto-char (match-beginning 1))
                         ;; if previous is a newline, don't include it i the overklay
-                        (when (looking-back "\\s-") (goto-char (- (point) 1)))
+                        (when (looking-back "\\s-" (1- (point)))
+                          (goto-char (- (point) 1)))
                         (point))))
             ; if several hyp names, we name the overlays with the first hyp name
             (setq res