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-shell.el | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'generic/proof-shell.el') diff --git a/generic/proof-shell.el b/generic/proof-shell.el index b5bbcd9f..51d10c2c 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.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 @@ -34,9 +34,8 @@ (declare-function proof-tree-urgent-action "proof-tree" (flags)) (declare-function proof-tree-handle-delayed-output "proof-tree" (old-proof-marker cmd flags span)) -(eval-when-compile - ;; without the nil initialization the compiler still warns about this variable - (defvar proof-tree-external-display nil)) +;; without the nil initialization the compiler still warns about this variable +(defvar proof-tree-external-display) (require 'scomint) (require 'pg-response) @@ -454,8 +453,7 @@ process command." ;; Call multiple-frames-enable in case we need to fire up ;; new frames (NB: sets specifiers to remove modeline) (save-selected-window - (save-selected-frame - (proof-multiple-frames-enable))))) + (proof-multiple-frames-enable)))) (message "Starting %s process... done." proc)))) -- 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-shell.el | 30 ++++++++++++++---------------- 1 file changed, 14 insertions(+), 16 deletions(-) (limited to 'generic/proof-shell.el') diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 51d10c2c..a176283d 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1,4 +1,4 @@ -;;; proof-shell.el --- Proof General shell mode. +;;; proof-shell.el --- Proof General shell mode ;; This file is part of Proof General. @@ -22,7 +22,7 @@ ;;; Code: -(require 'cl) ; set-difference, every +(require 'cl-lib) ; cl-set-difference, cl-every (eval-when-compile (require 'span) @@ -41,7 +41,7 @@ (require 'pg-response) (require 'pg-goals) (require 'pg-user) ; proof-script, new-command-advance - +(require 'span) ;; ;; Internal variables used by proof shell @@ -504,7 +504,7 @@ shell buffer, called by `proof-shell-bail-out' if process exits." (while (and (> timecount 0) (scomint-check-proc proof-shell-buffer)) (accept-process-output proc 1 nil 1) - (decf timecount))) + (cl-decf timecount))) ;; Still there, kill it rudely. (when (memq (process-status proc) '(open run stop)) @@ -890,7 +890,7 @@ inserted text. Do not use this function directly, or output will be lost. It is only used in `proof-add-to-queue' when we start processing a queue, and in `proof-shell-exec-loop', to process the next item." - (assert (or (stringp strings) + (cl-assert (or (stringp strings) (listp strings)) nil "proof-shell-insert: expected string list argument") @@ -1008,7 +1008,7 @@ being processed." (unless (eq proof-shell-busy queuemode) (proof-debug "proof-append-alist: wrong queuemode detected for busy shell") - (assert (eq proof-shell-busy queuemode))))) + (cl-assert (eq proof-shell-busy queuemode))))) (let ((nothingthere (null proof-action-list))) @@ -1182,7 +1182,7 @@ contains only invisible elements for Prooftree synchronization." (and (not proof-second-action-list-active) (or (null proof-action-list) - (every + (cl-every (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) proof-action-list))))))) @@ -1310,8 +1310,8 @@ to `proof-register-possibly-new-processed-file'." ;; the proof-shell-compute-new-files-list (proof-restart-buffers (proof-files-to-buffers - (set-difference current-included - proof-included-files-list))) + (cl-set-difference current-included + proof-included-files-list))) (cond ;; Do nothing if there was no active scripting buffer ((not scrbuf)) @@ -1762,7 +1762,7 @@ Only works when system timer has microsecond count available." (and (< (- tm pg-last-tracing-output-time) (/ pg-fast-tracing-mode-threshold 1000000.0)) - (>= (incf pg-last-trace-output-count) + (>= (cl-incf pg-last-trace-output-count) pg-slow-mode-trigger-count)) ;; quickly consecutive tracing outputs: go into slow mode (setq dontprint t) @@ -1856,16 +1856,14 @@ The flag 'invisible is always added to FLAGS." (not proof-shell-auto-terminate-commands) (string-match (concat (regexp-quote proof-terminal-string) - "[ \t]*$") cmd)) + "[ \t]*$") + cmd)) (setq cmd (concat cmd proof-terminal-string))) (if wait (proof-shell-wait)) (proof-shell-ready-prover) ; start proof assistant; set vars. (let* ((callback - (if invisiblecallback - (lexical-let ((icb invisiblecallback)) - (lambda (span) - (funcall icb span))) - 'proof-done-invisible))) + (or invisiblecallback + #'proof-done-invisible))) (proof-start-queue nil nil (list (proof-shell-action-list-item cmd -- cgit v1.2.3