From a921439a4eb5b0d96182748e779c78e2f6a41a5f Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Tue, 11 Dec 2018 18:48:51 -0500 Subject: Cleanup patch; Moving defvar to toplevel Move `defvar`s used to silence warnings outside of eval-when-compile. Make sure they don't actually give a value to the var. * pg-init.el: Simplify. Use (if t ...) to avoid running `require` at compile-time. Don't add subdirs to load-path here since this code is never used. (pg-init--script-full-path, pg-init--pg-root): Inline their definition into their sole user. * generic/proof-utils.el (proof-resize-window-tofit): Inline definitions of window-leftmost-p and window-rightmost-p previously in proof-compat.el. * lib/proof-compat.el (proof-running-on-win32): Remove, not used. (mac-key-mode): Remove, there's no carbon-emacs-package-version in Emacs≥24.3. (pg-custom-undeclare-variable): Use dolist. (save-selected-frame): Remove, save-selected-window also saves&restores the selected frame at the same time. Update all users (which already used save-selected-window around it). (window-leftmost-p, window-rightmost-p, window-bottom-p) (find-coding-system): Remove, unused. * hol-light/hol-light.el (caml-font-lock-keywords): Don't try to defvar it to a dummy value and... (hol-light): ...check its existence before using it instead. * coq/coq.el (coq-may-use-prettify): Simplify initialization. --- generic/proof-menu.el | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'generic/proof-menu.el') diff --git a/generic/proof-menu.el b/generic/proof-menu.el index fc18d504..027d0c7d 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.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 @@ -19,9 +19,8 @@ ;;; Code: (require 'cl) ; mapcan -(eval-when-compile - (defvar proof-assistant-menu) ; defined by macro in proof-menu-define-specific - (defvar proof-mode-map)) +(defvar proof-assistant-menu) ; defined by macro in proof-menu-define-specific +(defvar proof-mode-map) (require 'proof-utils) ; proof-deftoggle, proof-eval-when-ready-for-assistant (require 'proof-useropts) -- cgit v1.2.3 From 632a3d7f9ded16faaf58e1c0769bcd4f7c8193e3 Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Wed, 12 Dec 2018 15:20:08 -0500 Subject: 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. --- generic/proof-menu.el | 33 ++++++++++++++++++--------------- 1 file changed, 18 insertions(+), 15 deletions(-) (limited to 'generic/proof-menu.el') diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 027d0c7d..e43efcc0 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -17,7 +17,7 @@ ;; ;;; Code: -(require 'cl) ; mapcan +(require 'cl-lib) ; cl-mapcan, ... (defvar proof-assistant-menu) ; defined by macro in proof-menu-define-specific (defvar proof-mode-map) @@ -49,24 +49,26 @@ without adjusting window layout." (cond ((and (called-interactively-p 'any) (eq last-command 'proof-display-some-buffers)) - (incf proof-display-some-buffers-count)) + (cl-incf proof-display-some-buffers-count)) (t (setq proof-display-some-buffers-count 0))) - (let* ((assocbufs (remove-if-not 'buffer-live-p - (list proof-response-buffer - proof-thms-buffer - proof-trace-buffer - proof-goals-buffer - ))) + (let* ((assocbufs (cl-remove-if-not #'buffer-live-p + (list proof-response-buffer + proof-thms-buffer + proof-trace-buffer + proof-goals-buffer + ))) ;proof-shell-buffer (numassoc (length assocbufs))) ;; If there's no live other buffers, we don't do anything. (unless (zerop numassoc) (let ((selectedbuf (nth (mod proof-display-some-buffers-count - numassoc) assocbufs)) + numassoc) + assocbufs)) (nextbuf (nth (mod (1+ proof-display-some-buffers-count) - numassoc) assocbufs))) + numassoc) + assocbufs))) (cond ((or proof-three-window-enable proof-multiple-frames-enable) ;; Display two buffers: next in rotation and goals/response @@ -74,7 +76,8 @@ without adjusting window layout." (proof-switch-to-buffer selectedbuf 'noselect) (proof-switch-to-buffer (if (eq selectedbuf proof-goals-buffer) proof-response-buffer - proof-goals-buffer) 'noselect)) + proof-goals-buffer) + 'noselect)) (selectedbuf (proof-switch-to-buffer selectedbuf 'noselect))) (if (eq selectedbuf proof-response-buffer) @@ -755,7 +758,7 @@ suitable for adding to the proof assistant menu." (while (and new (fboundp menu-fn)) (setq menu-fn (intern (concat (symbol-name menuname-sym) "-" (int-to-string i)))) - (incf i)) + (cl-incf i)) (if inscript (eval `(proof-defshortcut ,menu-fn ,command ,key)) (eval `(proof-definvisible ,menu-fn ,command ,key))) @@ -789,7 +792,7 @@ suitable for adding to the proof assistant menu." nil t))) (let* ((favs (proof-ass favourites)) - (rmfavs (remove-if + (rmfavs (cl-remove-if (lambda (f) (string-equal menuname (caddr f))) favs))) (unless (equal favs rmfavs) @@ -831,7 +834,7 @@ KEY is the optional key binding." (let* ((menu-entry (proof-def-favourite command inscript menuname key t)) (favs (proof-ass favourites)) - (rmfavs (remove-if + (rmfavs (cl-remove-if (lambda (f) (string-equal menuname (caddr f))) favs)) (newfavs (append @@ -860,7 +863,7 @@ KEY is the optional key binding." (mapc (lambda (stg) (add-to-list 'groups (get (car stg) 'pggroup))) proof-assistant-settings) (dolist (grp (reverse groups)) - (let* ((gstgs (mapcan (lambda (stg) + (let* ((gstgs (cl-mapcan (lambda (stg) (if (eq (get (car stg) 'pggroup) grp) (list stg))) proof-assistant-settings)) -- cgit v1.2.3