Use `cl-lib` instead of `cl` everywhere

Use lexical-binding in a few files where it was easy.
Don't require `proof-compat` when it's not used.

* coq/coq-db.el: Use lexical-binding.

* coq/coq-system.el: Use lexical-binding.
(coq--extract-prog-args): Use concatenated-args rather than recomputing it.

* coq/coq.el: Require `span` to silence some warnings.

* generic/pg-user.el: Use lexical-binding.
(complete, add-completion, completion-min-length): Silence warnings.

* generic/pg-xml.el: Use lexical-binding.
(pg-xml-string-of): Prefer mapconcat to reduce+concat.

* generic/proof-depends.el: Use lexical-binding.
(proof-dep-split-deps): Use `push`.

* generic/proof-shell.el: Require `span` to silence some warnings.
(proof-shell-invisible-command): Don't use lexical-let just to build
a wasteful η-redex!

* lib/holes.el: Use lexical-binding.
Remove redundant :group args.

* lib/span.el: Use lexical-binding.
(span-read-only-hook): Use user-error.
(span-raise): Remove, unused.

6 files changed, 70 insertions, 84 deletions

diff --git a/lib/holes.el b/lib/holes.el
index 9a45037c..84dcf1f3 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -1,9 +1,9 @@
-;;; holes.el --- a little piece of elisp to define holes in your buffer
+;;; holes.el --- a little piece of elisp to define holes in your buffer  -*- 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
@@ -36,7 +36,7 @@
 
 ;;; Code:
 (require 'span)
-(require 'cl)
+(eval-when-compile (require 'cl-lib))
 
 ;;;
 ;;; initialization
@@ -65,16 +65,14 @@ and this is this one.  This is not buffer local.")
 
 (defcustom holes-empty-hole-string "#"
   "String to be inserted for empty hole (don't put an empty string)."
-  :type 'string
-  :group 'holes)
+  :type 'string)
 
 (defcustom holes-empty-hole-regexp "#\\|@{\\([^{}]*\\)}"
   "Regexp denoting a hole in abbrevs.
 Subgroup 1 is treated specially: if it matches, it is assumed that
 everything before it and after it in the regexp matches delimiters
 which should be removed when making the text into a hole."
-  :type 'regexp
-  :group 'holes)
+  :type 'regexp)
 
 
 ;(defcustom holes-search-limit 1000
@@ -97,8 +95,7 @@ which should be removed when making the text into a hole."
      :background "darkred" :foreground "white")
     (((class color) (background light))
      :background "paleVioletRed" :foreground "black"))
-  "Font Lock face used to highlight the active hole."
-  :group 'holes)
+  "Font Lock face used to highlight the active hole.")
 
 (defface inactive-hole-face
   '((((class grayscale) (background light)) :background "lightgrey")
@@ -107,8 +104,7 @@ which should be removed when making the text into a hole."
      :background "mediumblue" :foreground "white")
     (((class color) (background light))
      :background "lightsteelblue" :foreground "black"))
-  "Font Lock  face used to highlight the active hole."
-  :group 'holes)
+  "Font Lock  face used to highlight the active hole.")
 
 ;;;
 ;;; Keymaps
@@ -180,7 +176,7 @@ This is not the keymap used on holes's overlay (see `hole-map' instead).")
 
 (defun holes-copy-active-region ()
   "Copy and retuurn the active region."
-  (assert mark-active nil "the region is not active now.")
+  (cl-assert mark-active nil "the region is not active now.")
   (copy-region-as-kill (region-beginning) (region-end))
   (car kill-ring))
 
@@ -190,19 +186,19 @@ This is not the keymap used on holes's overlay (see `hole-map' instead).")
 
 (defun holes-hole-start-position (hole)
   "Return start position of HOLE."
-  (assert (holes-is-hole-p hole) t
+  (cl-assert (holes-is-hole-p hole) t
 	  "holes-hole-start-position: %s is not a hole")
   (span-start hole))
 
 (defun holes-hole-end-position (hole)
   "Return end position of HOLE."
-  (assert (holes-is-hole-p hole) t "holes-hole-end-position: %s is not a hole")
+  (cl-assert (holes-is-hole-p hole) t "holes-hole-end-position: %s is not a hole")
   (span-end hole))
 
 (defun holes-hole-buffer (hole)
   "Return the buffer of HOLE."
   "Internal."
-  (assert (holes-is-hole-p hole) t "holes-hole-buffer: %s is not a hole")
+  (cl-assert (holes-is-hole-p hole) t "holes-hole-buffer: %s is not a hole")
   (span-buffer hole))
 
 (defun holes-hole-at (&optional pos)
@@ -221,7 +217,7 @@ active-hole-marker variable)."
   "Return the position of the start of the active hole.
 See `active-hole-buffer' to get its buffer.  Returns an error if
 active hole doesn't exist (the marker is set to nothing)."
-  (assert (holes-active-hole-exist-p) t
+  (cl-assert (holes-active-hole-exist-p) t
 	  "holes-active-hole-start-position: no active hole")
   (holes-hole-start-position holes-active-hole))
 
@@ -229,7 +225,7 @@ active hole doesn't exist (the marker is set to nothing)."
   "Return the position of the start of the active hole.
 See `active-hole-buffer' to get its buffer.  Returns an error if
 active hole doesn't exist (the marker is set to nothing)."
-  (assert (holes-active-hole-exist-p) t
+  (cl-assert (holes-active-hole-exist-p) t
 	  "holes-active-hole-end-position: no active hole")
   (holes-hole-end-position holes-active-hole))
 
@@ -238,7 +234,7 @@ active hole doesn't exist (the marker is set to nothing)."
   "Return the buffer containing the active hole.
 Raise an error if the active hole is not set.  Don't care if the
 active hole is empty."
-  (assert (holes-active-hole-exist-p) t
+  (cl-assert (holes-active-hole-exist-p) t
 	  "holes-active-hole-buffer: no active hole")
   (holes-hole-buffer holes-active-hole))
 
@@ -246,7 +242,7 @@ active hole is empty."
   "Set point to active hole.
 Raises an error if active-hole is not set."
   (interactive)
-  (assert (holes-active-hole-exist-p) t
+  (cl-assert (holes-active-hole-exist-p) t
 	  "holes-goto-active-hole: no active hole")
   (goto-char (holes-active-hole-start-position)))
 
@@ -255,7 +251,7 @@ Raises an error if active-hole is not set."
   "Highlight a HOLE with the `active-hole-face'.
 DON'T USE this as it would break synchronization (non active hole
 highlighted)."
-  (assert (holes-is-hole-p hole) t
+  (cl-assert (holes-is-hole-p hole) t
 	  "holes-highlight-hole-as-active: %s is not a hole")
   (set-span-face hole 'active-hole-face))
 
@@ -263,7 +259,7 @@ highlighted)."
   "Highlight a HOLE with the not active face.
 DON'T USE this as it would break synchronization (active hole non
 highlighted)."
-  (assert (holes-is-hole-p hole) t
+  (cl-assert (holes-is-hole-p hole) t
 	  "holes-highlight-hole: %s is not a hole")
   (set-span-face hole 'inactive-hole-face))
 
@@ -283,7 +279,7 @@ the active hole is already disable."
 (defun holes-set-active-hole (hole)
   "Set active hole to HOLE.
 Error if HOLE is not a hole."
-  (assert (holes-is-hole-p hole) t
+  (cl-assert (holes-is-hole-p hole) t
 	  "holes-set-active-hole: %s is not a hole")
   (if (holes-active-hole-exist-p)
       (holes-highlight-hole holes-active-hole))
@@ -328,7 +324,7 @@ the span."
 
 (defun holes-clear-hole (hole)
   "Clear the HOLE."
-  (assert (holes-is-hole-p hole) t
+  (cl-assert (holes-is-hole-p hole) t
 	  "holes-clear-hole: %s is not a hole")
   (if (and (holes-active-hole-exist-p)
 	   (eq holes-active-hole hole))
@@ -363,11 +359,11 @@ Operate betwenn START and END if non nil."
 Or after the hole at pos if there is one (default pos=point).  If no
 hole found, return nil."
   (holes-map-holes
-   (lambda (h x) (and (holes-is-hole-p h) h)) buffer pos))
+   (lambda (h _) (and (holes-is-hole-p h) h)) buffer pos))
 
 (defun holes-next-after-active-hole ()
   "Internal."
-  (assert (holes-active-hole-exist-p) t
+  (cl-assert (holes-active-hole-exist-p) t
 	  "next-active-hole: no active hole")
   (holes-next (holes-active-hole-end-position)
 	      (holes-active-hole-buffer)))
@@ -441,7 +437,7 @@ goal(FIXME?).  Use `replace-active-hole' instead."
 Like `holes-replace-active-hole', but then sets the active hole to the
 following hole if it exists."
   (interactive)
-  (assert (holes-active-hole-exist-p) t
+  (cl-assert (holes-active-hole-exist-p) t
 	  "holes-replace-update-active-hole: no active hole")
   (if (holes-active-hole-exist-p)
       (let ((nxthole (holes-next-after-active-hole)))
@@ -560,9 +556,9 @@ Sets `holes-active-hole' to the next hole if it exists."
   "Move the point to current active hole (if any and if in current buffer).
 Destroy it and makes the next hole active if any."
   (interactive)
-  (assert (holes-active-hole-exist-p) nil "no active hole")
-  (assert (eq (current-buffer) (holes-active-hole-buffer)) nil
-	  "active hole not in this buffer")
+  (cl-assert (holes-active-hole-exist-p) nil "no active hole")
+  (cl-assert (eq (current-buffer) (holes-active-hole-buffer)) nil
+	     "active hole not in this buffer")
   (holes-goto-active-hole)
   (holes-delete-update-active-hole))
 
@@ -593,7 +589,7 @@ The LIMIT argument bounds the search; it is a buffer position.
   (let ((n 0))
     (save-excursion
       (while (re-search-backward holes-empty-hole-regexp limit t)
-	(incf n)
+	(cl-incf n)
 	(if (not (match-end 1))
 	    (holes-make-hole (match-beginning 0) (match-end 0))
 	  (holes-make-hole (match-beginning 1) (match-end 1))
@@ -625,12 +621,12 @@ If NOINDENT is non-nil, skip the indenting step.
 If ALWAYSJUMP is non-nil, jump to the first hole even if more than one."
   (unless noindent (save-excursion (indent-region pos (point) nil)))
   (let ((n (holes-replace-string-by-holes-backward pos)))
-    (case n
-      (0 nil)				; no hole, stay here.
-      (1
+    (pcase n
+      (`0 nil)				; no hole, stay here.
+      (`1
        (goto-char pos)
        (holes-set-point-next-hole-destroy)) ; if only one hole, go to it.
-      (t
+      (_
        (goto-char pos)
        (when alwaysjump (holes-set-point-next-hole-destroy))
        (unless (active-minibuffer-window) ; otherwise minibuffer gets hidden
@@ -727,10 +723,9 @@ it mean anyway?)
  o Cutting or pasting a hole will not produce new holes, and
 undoing on holes cannot make holes re-appear."
   nil " Holes" holes-mode-map
-  :group 'holes
   (if holes-mode
-      (add-hook 'skeleton-end-hook 'holes-skeleton-end-hook nil t)
-    (remove-hook 'skeleton-end-hook 'holes-skeleton-end-hook t)
+      (add-hook 'skeleton-end-hook #'holes-skeleton-end-hook nil t)
+    (remove-hook 'skeleton-end-hook #'holes-skeleton-end-hook t)
     (holes-clear-all-buffer-holes)))
 
 ;;;###autoload
diff --git a/lib/pg-dev.el b/lib/pg-dev.el
index 8e82a753..78d79862 100644
--- a/lib/pg-dev.el
+++ b/lib/pg-dev.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
@@ -24,9 +24,6 @@
 (require 'whitespace)
 
 (eval-when-compile
-  (require 'cl))
-
-(eval-when-compile
   (require 'proof-site))
 
 (with-no-warnings
diff --git a/lib/proof-compat.el b/lib/proof-compat.el
index 25c029c6..95c533e5 100644
--- a/lib/proof-compat.el
+++ b/lib/proof-compat.el
@@ -28,7 +28,7 @@
 
 ;;; Code:
 
-(require 'cl)
+(require 'cl-lib)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
@@ -63,7 +63,7 @@ in the current Emacs session."
 	     saved-value
 	     theme-value
 	     theme-face))
-    (remprop symbol prop)))
+    (cl-remprop symbol prop)))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/lib/span.el b/lib/span.el
index e7e3d68b..4bb7507e 100644
--- a/lib/span.el
+++ b/lib/span.el
@@ -1,9 +1,9 @@
-;;; span.el --- Datatype of "spans" for Proof General
+;;; span.el --- Datatype of "spans" for Proof General  -*- 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
@@ -24,8 +24,6 @@
 
 ;;; Code:
 
-(eval-when-compile (require 'cl))       ;For lexical-let.
-
 (defalias 'span-start 'overlay-start)
 (defalias 'span-end 'overlay-end)
 (defalias 'span-set-property 'overlay-put)
@@ -42,10 +40,9 @@
   "Check if an overlay OL belongs to PG."
   (overlay-get ol 'pg-span))
 
-(defun span-read-only-hook (overlay after start end &optional len)
+(defun span-read-only-hook (&rest _)
   (unless inhibit-read-only
-    (error "Region is read-only")))
-(add-to-list 'debug-ignored-errors "Region is read-only")
+    (user-error "Region is read-only")))
 
 (defun span-read-only (span)
   "Set SPAN to be read only."
@@ -61,12 +58,11 @@
 
 (defun span-write-warning (span fun)
   "Give a warning message when SPAN is changed, unless `inhibit-read-only' is non-nil."
-  (lexical-let ((fun fun))
-    (let ((funs (list (lambda (span afterp beg end &rest args)
-			(if (and (not afterp) (not inhibit-read-only))
-			    (funcall fun beg end))))))
-      (span-set-property span 'modification-hooks funs)
-      (span-set-property span 'insert-in-front-hooks funs))))
+  (let ((funs (list (lambda (_span afterp beg end &rest _)
+		      (if (and (not afterp) (not inhibit-read-only))
+			  (funcall fun beg end))))))
+    (span-set-property span 'modification-hooks funs)
+    (span-set-property span 'insert-in-front-hooks funs)))
 
 ;; We use end first because proof-locked-queue is often changed, and
 ;; its starting point is always 1
@@ -155,13 +151,13 @@ A span is before PT if it begins before the character before PT."
        (overlay-buffer span)
        (buffer-live-p (overlay-buffer span))))
 
-(defun span-raise (span)
-  "Set priority of SPAN to make it appear above other spans."
-  ;; FIXME: Emacs already uses a "shorter goes above" which takes care of
-  ;; preventing a span from seeing another.  So don't play with
-  ;; priorities, please!
-  ;; (span-set-property span 'priority 100)
-  )
+;; (defun span-raise (_span)
+;;   "Set priority of SPAN to make it appear above other spans."
+;;   ;; FIXME: Emacs already uses a "shorter goes above" which takes care of
+;;   ;; preventing a span from seeing another.  So don't play with
+;;   ;; priorities, please!
+;;   ;; (span-set-property span 'priority 100)
+;;   )
 
 (defun span-string (span)
   (with-current-buffer (overlay-buffer span)
@@ -180,7 +176,7 @@ A span is before PT if it begins before the character before PT."
         (overlays-at (posn-point (event-start event)))
         (or prop 'span))))
 
-(defun fold-spans (f &optional buffer from to maparg ignored-flags prop val)
+(defun fold-spans (f &optional buffer from to maparg _ignored-flags prop val)
   (with-current-buffer (or buffer (current-buffer))
     (let ((ols (overlays-in (or from (point-min)) (or to (point-max))))
           res)
@@ -238,7 +234,7 @@ The span will remove itself after a timeout of 2 seconds."
     (add-timeout 2 'delete-overlay ol)
     ol))
 
-(defun span-delete-self-modification-hook (span &rest args)
+(defun span-delete-self-modification-hook (span &rest _)
   "Hook for overlay modification-hooks, which deletes SPAN."
   (if (span-live-p span)
       (span-delete span)))
@@ -252,7 +248,7 @@ Return the span."
       (overlay-put ol (car props) (cadr props))
       (setq props (cddr props)))
     (span-set-property ol 'modification-hooks
-                       (list 'span-delete-self-modification-hook))
+                       (list #'span-delete-self-modification-hook))
     ol))
 
 
diff --git a/lib/texi-docstring-magic.el b/lib/texi-docstring-magic.el
index e39ee51a..2d6a3cf4 100644
--- a/lib/texi-docstring-magic.el
+++ b/lib/texi-docstring-magic.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
@@ -92,9 +92,6 @@
 
 ;;; Code:
 
-(eval-when-compile
-  (require 'cl))
-
 (defun texi-docstring-magic-find-face (face)
   "Return non-nil if FACE is a face name; nil otherwise.
 A face name can be a string or a symbol.
diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el
index 4d1d0d35..41f478d1 100644
--- a/lib/unicode-tokens.el
+++ b/lib/unicode-tokens.el
@@ -46,7 +46,7 @@
 
 ;;; Code:
 
-(require 'cl)
+(require 'cl-lib)
 (require 'quail)
 
 (eval-when-compile
@@ -429,12 +429,12 @@ This function also initialises the important tables for the mode."
     ;; hairy logic based on Coq-style vs Isabelle-style configs
     (if (string= "" (format unicode-tokens-token-format ""))
 	;; no special token format, parse separate words/symbols
- 	(let* ((tokextra (remove* "^\\(?:\\sw\\|\\s_\\)+$" toks :test 'string-match))
-               (toksymbwrd (set-difference toks tokextra))
+ 	(let* ((tokextra (cl-remove "^\\(?:\\sw\\|\\s_\\)+$" toks :test 'string-match))
+               (toksymbwrd (cl-set-difference toks tokextra))
                ;; indentifier that are not pure words
-               (toksymb (remove* "^\\(?:\\sw\\)+$" toksymbwrd :test 'string-match))
+               (toksymb (cl-remove "^\\(?:\\sw\\)+$" toksymbwrd :test 'string-match))
                ;; pure words
-               (tokwrd (set-difference toksymbwrd toksymb))
+               (tokwrd (cl-set-difference toksymbwrd toksymb))
 	       (idorop
 		(concat "\\(\\_<"
                         (regexp-opt toksymb)
@@ -461,9 +461,9 @@ This function also initialises the important tables for the mode."
 The check is with `char-displayable-p'."
   (cond
    ((stringp comp)
-    (reduce (lambda (x y) (and x (char-displayable-p y)))
- 	    comp
- 	    :initial-value t))
+    (cl-reduce (lambda (x y) (and x (char-displayable-p y)))
+ 	       comp
+ 	       :initial-value t))
    ((characterp comp)
     (char-displayable-p comp))
    (comp ;; assume any other non-null is OK
@@ -518,7 +518,7 @@ The face property is set to the :family and :slant attriubutes taken from
 					    (car props) (cadr props))
 	    (setq props (cddr props)))))
     (unless (or unicode-tokens-show-symbols
-		(intersection unicode-tokens-fonts propsyms))
+		(cl-intersection unicode-tokens-fonts propsyms))
       (font-lock-append-text-property
        start end 'face
        ;; just use family and slant to enhance merging with other faces
@@ -680,7 +680,7 @@ Calculated from `unicode-tokens-token-name-alist' and
 `unicode-tokens-shortcut-alist'."
   (let ((unicode-tokens-quail-define-rules
 	 (list 'quail-define-rules)))
-    (let ((ulist (copy-list unicode-tokens-shortcut-alist))
+    (let ((ulist (copy-sequence unicode-tokens-shortcut-alist))
 	  ustring shortcut)
       (setq ulist (sort ulist 'unicode-tokens-map-ordering))
       (while ulist
@@ -714,7 +714,7 @@ Available annotations chosen from `unicode-tokens-control-regions'."
 			"Annotate region with: "
 			unicode-tokens-control-regions nil
 			'requirematch))))
-  (assert (assoc name unicode-tokens-control-regions))
+  (cl-assert (assoc name unicode-tokens-control-regions))
   (let* ((entry (assoc name unicode-tokens-control-regions))
 	 (beg   (region-beginning))
 	 (end   (region-end))
@@ -736,7 +736,7 @@ Available annotations chosen from `unicode-tokens-control-regions'."
 		      "Insert control symbol: "
 		      unicode-tokens-control-characters
 		      nil 'requirematch)))
-  (assert (assoc name unicode-tokens-control-characters))
+  (cl-assert (assoc name unicode-tokens-control-characters))
   (insert (format unicode-tokens-control-char-format
 		  (cadr (assoc name unicode-tokens-control-characters)))))
 
@@ -833,7 +833,8 @@ but multiple characters in the underlying buffer."
 	    (error "Cannot find token before point"))
 	  (when token
 	    (let* ((tokennumber
-		    (search (list token) unicode-tokens-token-list :test 'equal))
+		    (cl-search (list token) unicode-tokens-token-list
+                               :test #'equal))
 		   (numtoks
 		    (hash-table-count unicode-tokens-hash-table))
 		   (newtok
@@ -943,7 +944,7 @@ Starts from point."
 			     'face
 			     'header-line))
 	    (insert " "))
-	  (incf count)
+	  (cl-incf count)
 	  (if (null toks)
 	      (insert " ")
 	    (insert-text-button