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, 6 insertions, 42 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 308ca865..a15db325 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -1,9 +1,9 @@
-;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode
+;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -68,46 +68,10 @@
 
 ;;; The abbrev table built from keywords tables
 ;#s and @{..} are replaced by holes by holes-abbrev-complete
-(defun coq-install-abbrevs ()
-  "Install default abbrev table for coq if no other already is."
-  (if (boundp 'coq-mode-abbrev-table)
-      ;; da: this test will always fail.  Assume bound-->non-empty
-      ;; (not (equal coq-mode-abbrev-table (make-abbrev-table))))
-      (message "Coq abbrevs already exists, default not loaded")
-    (define-abbrev-table 'coq-mode-abbrev-table
-      (append coq-tactics-abbrev-table coq-tacticals-abbrev-table
-              coq-commands-abbrev-table coq-terms-abbrev-table))
-    ;; if we use default coq abbrev, never ask to save it
-    ;; PC: fix trac #382 I comment this. But how to disable abbrev
-    ;; saving for coq mode only?
-    ;;(setq save-abbrevs nil) ; 
-    ;; DA: how about above, just temporarily disable saving?
-    (message "Coq default abbrevs loaded")))
-
-(unless (or noninteractive (bound-and-true-p byte-compile-current-file))
-  (coq-install-abbrevs))
-;;;;;
-
-; Redefining this macro to change the way a string option is asked to
-; the user: we pre fill the answer with current value of the option;
-(defun proof-defstringset-fn (var &optional othername)
-  "Define a function <VAR>-toggle for setting an integer customize setting VAR.
-Args as for the macro `proof-defstringset', except will be evaluated."
-  (eval
-   `(defun ,(if othername othername
-	      (intern (concat (symbol-name var) "-stringset"))) (arg)
-	      ,(concat "Set `" (symbol-name var) "' to ARG.
-This function simply uses customize-set-variable to set the variable.
-It was constructed with `proof-defstringset-fn'.")
-;	      (interactive ,(format "sValue for %s (a string, currenly %s): "
-;				    (symbol-name var) (symbol-value var)))
-	      (interactive (list
-			    (read-string
-			     (format "Value for %s (float): "
-				     (symbol-name (quote ,var))
-				     (symbol-value (quote ,var)))
-			     (symbol-value (quote ,var)))))
-	      (customize-set-variable (quote ,var) arg))))
+(define-abbrev-table 'coq-mode-abbrev-table
+  (append coq-tactics-abbrev-table coq-tacticals-abbrev-table
+          coq-commands-abbrev-table coq-terms-abbrev-table)
+  "Abbrev table for Coq.")
 
 ;; The coq menu partly built from tables