Fix remaining uses of CL; Make files more declarative

Emacs occasionally loads Elisp files just to get more info (e.g. for C-h f),
so loading a file should "no effect".  Fix the most obvious such effects:
the splash screen and the autotests by moving those effects into a function.

* coq/coq-autotest.el: Make it declarative.  Use lexical-binding.
(coq-autotest): New function holding the code that used to be at top-level.

* generic/proof.el: Use lexical-binding.
Don't call proof-splash-message just because we're being loaded.

* generic/proof-script.el: Use lexical-scoping; fix all warnings.
(pg-show-all-portions): Simplify the code with a closure.
(proof-activate-scripting): Declare activated-interactively as dyn-scoped.
(proof--splash-done): New var.
(proof-mode): Call proof-splash-message upon first use.

* generic/proof-splash.el (proof-splash-message): Don't check
byte-compile-current-file now that we're only called when the mode
is activated.

* acl2/acl2.el (auto-mode-alist): Use `add-to-list` and \'.

* coq/coq-db.el (coq-build-menu-from-db-internal): Avoid silly O(N²).

* coq/coq-seq-compile.el:
* coq/coq-par-test.el:
* coq/coq-par-compile.el: Fix leftover uses of CL's `assert`.

* generic/proof-utils.el:
* generic/pg-movie.el:
* etc/testsuite/pg-test.el:
* coq/coq-syntax.el: Fix leftover uses of CL's `incf`.

* generic/pg-autotest.el: Fix leftover uses of CL's `decf`.

* obsolete/plastic/plastic.el (plastic-preprocessing): Fix leftover use
of CL's `loop`.

* generic/pg-user.el (proof-add-completions): Do nothing if no
proof-assistant is set yet (i.e. during byte-compilation).
(byte-compile-current-file): No need to test this any more.

* generic/proof-syntax.el (proof-regexp-alt-list): Use mapconcat.
Remove unnecessary "\\(?:...\\)".
(proof-regexp-alt): Redefine in terms of proof-regexp-alt-list.

9 files changed, 78 insertions, 81 deletions

diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index e7cb19a9..7a22c9f7 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -3,7 +3,7 @@
 ;; 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
@@ -25,6 +25,7 @@
 
 ;;; Code:
 
+(eval-when-compile (require 'cl-lib))
 (require 'proof-splash)
 (setq proof-splash-enable nil)		; prevent splash when testing
 
@@ -215,7 +216,7 @@ completely processing the buffer as the last step."
 	 " random jump: processing whole buffer")
 	(proof-process-buffer)
 	(proof-shell-wait)
-	(decf jumps))
+	(cl-decf jumps))
 
 	((and (eq random-thing 1)
 	      (not (proof-locked-region-empty-p)))
@@ -223,7 +224,7 @@ completely processing the buffer as the last step."
 	  " random jump: retracting whole buffer")
 	 (proof-retract-buffer)
 	 (proof-shell-wait)
-	 (decf jumps))
+	 (cl-decf jumps))
 
 	(t
 	 (pg-autotest-message
@@ -241,7 +242,7 @@ completely processing the buffer as the last step."
 		    " random jump: interrupting prover")
 		   (proof-interrupt-process)))
 	     (proof-shell-wait))
-	   (decf jumps)))))
+	   (cl-decf jumps)))))
   (unless (proof-locked-region-full-p)
     (proof-process-buffer)
     (proof-shell-wait))
diff --git a/generic/pg-movie.el b/generic/pg-movie.el
index 9be95972..755d41f5 100644
--- a/generic/pg-movie.el
+++ b/generic/pg-movie.el
@@ -3,7 +3,7 @@
 ;; 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
@@ -30,6 +30,7 @@
 ;;
 
 ;;; Code:
+(eval-when-compile (require 'cl-lib))
 (eval-when-compile
   (require 'span)
   (require 'unicode-tokens))
@@ -72,7 +73,7 @@
 		    (t "command")))
 	 (label    (span-property span 'rawname))
 	 (frameid  (int-to-string pg-movie-frame)))
-    (incf pg-movie-frame)
+    (cl-incf pg-movie-frame)
     (pg-xml-node frame
 		 (list (pg-xml-attr frameNumber frameid))
 		 (list
diff --git a/generic/pg-user.el b/generic/pg-user.el
index a5ed27a9..57d29f18 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -558,18 +558,18 @@ last use time, to discourage saving these into the users database."
   (defvar completion-min-length)
   (declare-function add-completion "completion"
                     (string &optional num-uses last-use-time))
-  (mapcar (lambda (cmpl)
-	    ;; completion gives error; trapping is tricky so test again
-	    (if (>= (length cmpl) completion-min-length)
-		(add-completion cmpl -1000 0)))
-	  (proof-ass completion-table)))
+  (when proof-assistant
+    (mapcar (lambda (cmpl)
+	      ;; completion gives error; trapping is tricky so test again
+	      (if (>= (length cmpl) completion-min-length)
+		  (add-completion cmpl -1000 0)))
+	    (proof-ass completion-table))))
 
 ;; NB: completion table is expected to be set when proof-script
 ;; is loaded!  Call `proof-script-add-completions' to update.
 
-(unless (bound-and-true-p byte-compile-current-file) ;FIXME: Yuck!
-  (eval-after-load "completion"
-    '(proof-add-completions)))
+(eval-after-load "completion"
+  '(proof-add-completions))
 
 (defun proof-script-complete (&optional arg)
   "Like `complete' but case-fold-search set to `proof-case-fold-search'."
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 4c56fc7b..f8cf0cab 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1,4 +1,4 @@
-;;; proof-script.el --- Major mode for proof assistant script files.
+;;; proof-script.el --- Major mode for proof assistant script files.  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -42,6 +42,7 @@
 (declare-function proof-segment-up-to "proof-script")
 (declare-function proof-autosend-enable "pg-user")
 (declare-function proof-interrupt-process "pg-shell")
+(declare-function proof-cd-sync "pg-user" ())
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -142,7 +143,7 @@ scripting buffer may have an active queue span.")
 
 ;; ** Getters and setters
 
-(defun proof-span-give-warning (&rest args)
+(defun proof-span-give-warning (&rest _args)
   "Give a warning message.
 Optional argument ARGS is ignored."
   (unless inhibit-read-only
@@ -506,7 +507,7 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
 (defun pg-clear-script-portions ()
   "Clear record of script portion names and types from internal list."
   (dolist (idtbl pg-script-portions)
-    (maphash (lambda (k span) (span-delete span)) (cdr idtbl))
+    (maphash (lambda (_k span) (span-delete span)) (cdr idtbl))
     (clrhash (cdr idtbl))))
 
 (defun pg-remove-element (idiom id)
@@ -628,14 +629,11 @@ IDIOMSYM is a symbol and ID is a strings."
       (concat "Make "
 	      (if current-prefix-arg "in" "")
 	      "visible all regions of: ")
-      (apply 'vector pg-idioms) nil t))
+      (apply #'vector pg-idioms) nil t))
     current-prefix-arg))
   (let ((elts    (cdr-safe (assq idiom pg-script-portions)))
-	(alterfn (if hide
-		     (lambda (k span)
-		       (pg-set-element-span-invisible span t))
-		   (lambda (k span)
-		     (pg-set-element-span-invisible span nil)))))
+	(alterfn (lambda (_k span)
+		   (pg-set-element-span-invisible span hide))))
     (when elts
       (proof-with-script-buffer ; may be called from menu
        (maphash alterfn elts)))))
@@ -668,7 +666,6 @@ Each span has a 'type property, one of:
     'pbp	  A PBP command inserted automatically into the script."
   (let ((type    (span-property span 'type))
 	(idiom   (span-property span 'idiom))
-	(name    (span-property span 'name))
 	(rawname (span-property span 'rawname)))
     (cond
      (idiom
@@ -1213,10 +1210,10 @@ activation is considered to have failed and an error is given."
       ;; If there's another buffer currently active, we need to
       ;; deactivate it (also fixing up the included files list).
       (when proof-script-buffer
-	    (proof-deactivate-scripting)
-	    ;; Test whether deactivation worked
-	    (if proof-script-buffer
-		(error
+	(proof-deactivate-scripting)
+	;; Test whether deactivation worked
+	(if proof-script-buffer
+	    (error
 	     "You cannot have more than one active scripting buffer!")))
 
       ;; Ensure this buffer is off the included files list.  If we
@@ -1265,21 +1262,21 @@ activation is considered to have failed and an error is given."
       ;; block.  NB: The hook function may send commands to the
       ;; process which will re-enter this function, but should exit
       ;; immediately because scripting has been turned on now.
-      (if proof-activate-scripting-hook
-	  (let
-	      ((activated-interactively	(called-interactively-p 'any)))
-	    (setq proof-shell-last-output-kind nil)
-	    (run-hooks 'proof-activate-scripting-hook)
-	    ;; If activate scripting functions caused an error,
-	    ;; prevent switching to another buffer.  Might be better
-	    ;; to leave to specific instances, or simply run the hooks
-	    ;; as the last step before turning on scripting properly.
-	    (when (or (eq 'error proof-shell-last-output-kind)
-		      (eq 'interrupt proof-shell-last-output-kind))
-	      (proof-deactivate-scripting) ;; turn off again!
-	      ;; Give an error to prevent further actions.
-	      (error
-	       "Scripting not activated because of error or interrupt")))))))
+      (when proof-activate-scripting-hook
+        (defvar activated-interactively)
+	(let ((activated-interactively (called-interactively-p 'any)))
+	  (setq proof-shell-last-output-kind nil)
+	  (run-hooks 'proof-activate-scripting-hook)
+	  ;; If activate scripting functions caused an error,
+	  ;; prevent switching to another buffer.  Might be better
+	  ;; to leave to specific instances, or simply run the hooks
+	  ;; as the last step before turning on scripting properly.
+	  (when (or (eq 'error proof-shell-last-output-kind)
+		    (eq 'interrupt proof-shell-last-output-kind))
+	    (proof-deactivate-scripting) ;; turn off again!
+	    ;; Give an error to prevent further actions.
+	    (error
+	     "Scripting not activated because of error or interrupt")))))))
 
 
 (defun proof-toggle-active-scripting (&optional arg)
@@ -1415,7 +1412,8 @@ Argument SPAN has just been processed."
 						(span-end span)))
       (if (proof-string-match-safe proof-script-evaluate-elisp-comment-regexp str)
 	  (condition-case nil
-	      (eval (car (read-from-string (match-string-no-properties 1 str))))
+	      (eval (car (read-from-string (match-string-no-properties 1 str)))
+                    t)
 	    (t (proof-debug
 		(concat
 		 "lisp error when obeying proof-shell-evaluate-elisp-comment-regexp: \n"
@@ -1599,7 +1597,7 @@ Subroutine of `proof-done-advancing-save'."
       ;; start of the buffer, we make a fake goal-save region.
 
       ;; Delete spans between the previous goal and new command
-      (mapc 'span-delete dels)
+      (mapc #'span-delete dels)
 
       ;; Try to set the name from the goal... [as above]
       (setq nam (or (proof-get-name-from-goal gspan)
@@ -1643,7 +1641,7 @@ Subroutine of `proof-done-advancing-save'."
 ;; command syntax (terminated, not terminated, or lisp-style), whether
 ;; or not PG silently ignores comments, etc.
 
-(defun proof-segment-up-to-parser (pos &optional next-command-end)
+(defun proof-segment-up-to-parser (pos &optional _next-command-end)
   "Parse the script buffer from end of queue/locked region to POS.
 This partitions the script buffer into contiguous regions, classifying
 them by type.  Return a list of lists of the form
@@ -1838,7 +1836,7 @@ The optional QUEUEFLAGS are added to each queue item."
   (let ((start (proof-queue-or-locked-end))
 	(file  (or (buffer-file-name) (buffer-name)))
 	(cb    'proof-done-advancing)
-	span alist semi item end)
+	span alist end)
     (setq semis (nreverse semis))
     (save-match-data
       (dolist (semi semis)
@@ -1927,7 +1925,7 @@ always defaults to inserting a semi (nicer might be to parse for a
 comment, and insert or skip to the next semi)."
   (let ((mrk         (point))
 	(termregexp  (regexp-quote proof-terminal-string))
-	ins incomment nwsp)
+	ins nwsp)
     (if (< mrk (proof-unprocessed-begin))
 	(insert proof-terminal-string) ; insert immediately in locked region
       (if (proof-only-whitespace-to-locked-region-p)
@@ -1953,7 +1951,6 @@ comment, and insert or skip to the next semi)."
 	(unless semis
 	  (error "Can't find a parseable command!"))
 	(when (eq 'unclosed-comment (caar semis))
-	  (setq incomment t)
 	  ;; delete spurious char in comment
 	  (if ins (backward-delete-char 1))
 	  (goto-char mrk)
@@ -2258,17 +2255,22 @@ query saves here."
 ;; Proof General scripting mode definition, part 1.
 ;;
 
+(defvar proof--splash-done nil)
+
 ;;;###autoload
 (define-derived-mode proof-mode fundamental-mode
   proof-general-name
   "Proof General major mode class for proof scripts.
 \\{proof-mode-map}"
 
+  (unless (or proof--splash-done noninteractive)
+    (setq proof--splash-done t)
+    (proof-splash-message))
+
   (setq proof-buffer-type 'script)
 
   ;; Set default indent function (can be overriden in derived modes)
-  (make-local-variable 'indent-line-function)
-  (setq indent-line-function 'proof-indent-line)
+  (setq-local indent-line-function #'proof-indent-line)
 
   ;; During write-file it can happen that we re-set the mode for the
   ;; currently active scripting buffer.  The user might also do this
@@ -2286,9 +2288,9 @@ query saves here."
   (proof-script-set-after-change-functions)
 
   (add-hook 'after-set-visited-file-name-hooks
-	    'proof-script-set-visited-file-name nil t)
+	    #'proof-script-set-visited-file-name nil t)
 
-  (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t))
+  (add-hook 'proof-activate-scripting-hook #'proof-cd-sync nil t))
 
 ;; NB: proof-mode-map declared above
 (proof-menu-define-keys proof-mode-map)
@@ -2321,9 +2323,9 @@ This hook also gives a warning in case this is the active scripting buffer."
   "Set the hooks for a proof script buffer.
 The hooks set here are cleared by `write-file', so we use this function
 to restore them using `after-set-visited-file-name-hooks'."
-  (add-hook 'kill-buffer-hook 'proof-script-kill-buffer-fn t t)
+  (add-hook 'kill-buffer-hook #'proof-script-kill-buffer-fn t t)
   ;; Reverting buffer is same as killing it as far as PG is concerned
-  (add-hook 'before-revert-hook 'proof-script-kill-buffer-fn t t))
+  (add-hook 'before-revert-hook #'proof-script-kill-buffer-fn t t))
 
 (defun proof-script-kill-buffer-fn ()
   "Value of `kill-buffer-hook' for proof script buffers.
@@ -2616,17 +2618,17 @@ finish setup which depends on specific proof assistant configuration."
   "Choose parsing mechanism according to different kinds of script syntax.
 Choice of function depends on configuration setting."
   (unless (fboundp 'proof-segment-up-to)
-    (defalias 'proof-segment-up-to 'proof-segment-up-to-parser)
+    (defalias 'proof-segment-up-to #'proof-segment-up-to-parser)
     (cond
      (proof-script-parse-function
       ;; already set, nothing to do
       )
      (proof-script-sexp-commands
-      (setq proof-script-parse-function 'proof-script-generic-parse-sexp))
+      (setq proof-script-parse-function #'proof-script-generic-parse-sexp))
      (proof-script-command-start-regexp
-      (setq proof-script-parse-function 'proof-script-generic-parse-cmdstart))
+      (setq proof-script-parse-function #'proof-script-generic-parse-cmdstart))
      ((or proof-script-command-end-regexp proof-terminal-string)
-      (setq  proof-script-parse-function 'proof-script-generic-parse-cmdend)
+      (setq  proof-script-parse-function #'proof-script-generic-parse-cmdend)
       (unless proof-script-command-end-regexp
 	(proof-warn-if-unset "probof-config-done" 'proof-terminal-string)
 	(setq proof-script-command-end-regexp
@@ -2726,7 +2728,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.")
 		  (cdr semis))))
       usedsemis)))
 
-(defun proof-script-after-change-function (start end prelength)
+(defun proof-script-after-change-function (start _end _prelength)
   "Value for `after-change-functions' in proof script buffers."
   (setq proof-last-edited-low-watermark
 	(min (or proof-last-edited-low-watermark (point-max))
@@ -2741,7 +2743,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.")
 (defun proof-script-set-after-change-functions ()
   "Set `after-change-functions' for script buffers."
   (add-hook 'after-change-functions
-	    'proof-script-after-change-function nil t))
+	    #'proof-script-after-change-function nil t))
 
 
 
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index 75164890..600e9b4e 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -3,7 +3,7 @@
 ;; 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
@@ -270,7 +270,7 @@ binding to remove this buffer."
 (defun proof-splash-message ()
   "Make sure the user gets welcomed one way or another."
   (interactive)
-  (unless (or proof-splash-seen noninteractive (bound-and-true-p byte-compile-current-file))
+  (unless (or proof-splash-seen noninteractive)
     (if proof-splash-enable
 	(progn
 	  ;; disable ordinary emacs splash
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index e93f5ca4..d494279a 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -36,18 +36,14 @@ Uses a regexp of the form \\_<...\\_>."
 (defconst proof-no-regexp "\\<\\>"
   "A regular expression that never matches anything.")
 
-(defsubst proof-regexp-alt (&rest args)
+(defsubst proof-regexp-alt-list (args)
   "Return the regexp which matches any of the regexps ARGS."
-  ;; see regexp-opt (NB: but that is for strings, not regexps)
-  (let ((res ""))
-    (dolist (regexp args)
-      (setq res (concat res (if (string-equal res "") "\\(?:" "\\|\\(?:")
-			regexp "\\)")))
-    res))
+  (mapconcat #'identity args "\\|"))
 
-(defsubst proof-regexp-alt-list (args)
+(defsubst proof-regexp-alt (&rest args)
   "Return the regexp which matches any of the regexps ARGS."
-  (apply 'proof-regexp-alt args))
+  ;; see regexp-opt (NB: but that is for strings, not regexps)
+  (proof-regexp-alt-list args))
 
 (defsubst proof-re-search-forward-region (startre endre)
   "Search for a region delimited by regexps STARTRE and ENDRE.
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index 9a60e0ac..4ce51c99 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -3,7 +3,7 @@
 ;; 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
@@ -50,7 +50,7 @@ approximation we test whether proof-config is fully-loaded yet."
   (set-default sym value)
   (when (and
 	 (not noninteractive)
-	 (not (bound-and-true-p byte-compile-current-file))
+	 (not (bound-and-true-p byte-compile-current-file)) ;FIXME: Yuck!
 	 (featurep 'pg-custom)
 	 (featurep 'proof-config))
       (if (fboundp sym)
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 99e537c5..1568b2f0 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -23,6 +23,7 @@
 
 ;;; Code:
 
+(eval-when-compile (require 'cl-lib))
 ;;
 ;; Give Emacs version mismatch error here.
 ;;
@@ -58,8 +59,6 @@
 (require 'proof-autoloads)		; interface fns
 (require 'scomint)			; for proof-shell-live-buffer
 
-;;; Code:
-
 ;;
 ;; Handy macros
 ;;
@@ -247,7 +246,8 @@ Experimentally we display a message from time to time advertising
   ;; IF there *isn't* a visible window showing buffer...
   (unless (get-buffer-window buffer 0)
     (if proof-three-window-enable
-        (if (< proof-advertise-layout-count 30) (incf proof-advertise-layout-count)
+        (if (< proof-advertise-layout-count 30)
+            (cl-incf proof-advertise-layout-count)
           (message (substitute-command-keys "Hit \\[proof-layout-windows] to reset layout"))
           (setq proof-advertise-layout-count 0)))
     ;; THEN either we are in 2 wins mode and we must switch the assoc
diff --git a/generic/proof.el b/generic/proof.el
index f3b3b276..769459df 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -1,4 +1,4 @@
-;;; proof.el --- Proof General theorem prover interface
+;;; proof.el --- Proof General theorem prover interface  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -33,9 +33,6 @@
 
 (require 'proof-site)			; site/prover config, global vars, autoloads
 
-(unless (or noninteractive (bound-and-true-p byte-compile-current-file))
-  (proof-splash-message))		; welcome the user now.
-
 (require 'proof-utils)			; utilities
 (require 'proof-config)			; configuration variables
 (require 'proof-auxmodes)		; auxmode functions