diff options
author | Stefan Monnier <monnier@iro.umontreal.ca> | 2018-12-11 18:48:51 -0500 |
---|---|---|
committer | Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-12-12 12:28:39 -0500 |
commit | a921439a4eb5b0d96182748e779c78e2f6a41a5f (patch) | |
tree | a887ed306e13a0bcf21a939166322819bf669281 /coq | |
parent | 05df29f7ff065d8da45b81691c602b6cf075e4a0 (diff) |
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.
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq-compile-common.el | 9 | ||||
-rw-r--r-- | coq/coq-indent.el | 5 | ||||
-rw-r--r-- | coq/coq-local-vars.el | 7 | ||||
-rw-r--r-- | coq/coq-par-compile.el | 5 | ||||
-rw-r--r-- | coq/coq-seq-compile.el | 5 | ||||
-rw-r--r-- | coq/coq-system.el | 7 | ||||
-rw-r--r-- | coq/coq.el | 72 |
7 files changed, 49 insertions, 61 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 97ea6ec6..9dca0082 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.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 @@ -26,10 +26,9 @@ (require 'coq-system) (require 'compile) -(eval-when-compile - ;;(defvar coq-pre-v85 nil) - (defvar coq-confirm-external-compilation); defpacustom - (defvar coq-compile-parallel-in-background)) ; defpacustom +;;(defvar coq-pre-v85 nil) +(defvar coq-confirm-external-compilation); defpacustom +(defvar coq-compile-parallel-in-background) ; defpacustom ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 6e8ba013..af780251 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.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 @@ -33,8 +33,7 @@ ; ,@body ; (message "%.06f" (float-time (time-since time))))) -(eval-when-compile - (defvar coq-script-indent)) +(defvar coq-script-indent) (defconst coq-any-command-regexp (proof-regexp-alt-list coq-keywords)) diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el index b8c5d7e3..f172adbe 100644 --- a/coq/coq-local-vars.el +++ b/coq/coq-local-vars.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 @@ -22,9 +22,8 @@ (eval-when-compile (require 'cl)) -(eval-when-compile - (defvar coq-prog-name) - (defvar coq-load-path)) +(defvar coq-prog-name) +(defvar coq-load-path) (defconst coq-local-vars-doc nil diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index e3daebcd..b03fedaa 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.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 @@ -37,8 +37,7 @@ (eval-when-compile (require 'proof-compat)) -(eval-when-compile - (defvar queueitems)) ; dynamic scope in p-s-extend-queue-hook +(defvar queueitems) ; dynamic scope in p-s-extend-queue-hook (require 'coq-compile-common) diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index 5875908c..74327b53 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.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 @@ -27,8 +27,7 @@ (eval-when-compile (require 'proof-compat)) -(eval-when-compile - (defvar queueitems)) ; dynamic scope in p-s-extend-queue-hook +(defvar queueitems) ; dynamic scope in p-s-extend-queue-hook (require 'coq-compile-common) diff --git a/coq/coq-system.el b/coq/coq-system.el index 68d036f1..bb1c28f0 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.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 @@ -29,9 +29,8 @@ (require 'cl) (require 'proof-compat)) -(eval-when-compile - (defvar coq-prog-args) - (defvar coq-debug)) +(defvar coq-prog-args) +(defvar coq-debug) ;; Arbitrary arguments can already be passed through _CoqProject. ;; However this is not true for all assistants, so we don't modify the @@ -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 @@ -28,21 +28,20 @@ (require 'span) (require 'outline) (require 'newcomment) - (require 'etags) - (unless (proof-try-require 'smie) - (defvar smie-indent-basic) - (defvar smie-rules-function)) - (defvar proof-info) ; dynamic scope in proof-tree-urgent-action - (defvar action) ; dynamic scope in coq-insert-as stuff - (defvar string) ; dynamic scope in coq-insert-as stuff - (defvar old-proof-marker) - (defvar coq-keymap) - (defvar coq-one-command-per-line) - (defvar coq-auto-insert-as) ; defpacustom - (defvar coq-time-commands) ; defpacustom - (defvar coq-use-project-file) ; defpacustom - (defvar coq-use-editing-holes) ; defpacustom - (defvar coq-hide-additional-subgoals)) + (require 'etags)) +(defvar smie-indent-basic) +(defvar smie-rules-function) +(defvar proof-info) ; dynamic scope in proof-tree-urgent-action +(defvar action) ; dynamic scope in coq-insert-as stuff +(defvar string) ; dynamic scope in coq-insert-as stuff +(defvar old-proof-marker) +(defvar coq-keymap) +(defvar coq-one-command-per-line) +(defvar coq-auto-insert-as) ; defpacustom +(defvar coq-time-commands) ; defpacustom +(defvar coq-use-project-file) ; defpacustom +(defvar coq-use-editing-holes) ; defpacustom +(defvar coq-hide-additional-subgoals) (require 'proof) (require 'coq-system) ; load path, option, project file etc. @@ -66,11 +65,8 @@ ;; prettify is in emacs > 24.4 ;; FIXME: this should probably be done like for smie above. -(defvar coq-may-use-prettify nil) ; may become t below -(eval-when-compile - (if (fboundp 'prettify-symbols-mode) - (defvar coq-may-use-prettify t) - (defvar prettify-symbols-alist nil))) +(defvar coq-may-use-prettify (fboundp 'prettify-symbols-mode)) +(defvar prettify-symbols-alist) ;; ----- coq-shell configuration options @@ -911,22 +907,21 @@ This is mapped to control/shift mouse-1, unless coq-remap-mouse-1 is nil (t by default)." (interactive "e") (save-selected-window - (save-selected-frame - (save-excursion - (mouse-set-point event) - (let* ((id (coq-id-at-point)) - (notat (coq-notation-at-position (point))) - (modifs (event-modifiers event)) - (shft (member 'shift modifs)) - (ctrl (member 'control modifs)) - (cmd (when (or id notat) - (if (and ctrl shft) (if id "Check" "Locate") - (if shft (if id "About" "Locate") - (if ctrl (if id "Print" "Locate"))))))) - (proof-shell-invisible-command - (format (concat cmd " %s . ") - ;; Notation need to be surrounded by "" - (if id id (concat "\"" notat "\""))))))))) + (save-excursion + (mouse-set-point event) + (let* ((id (coq-id-at-point)) + (notat (coq-notation-at-position (point))) + (modifs (event-modifiers event)) + (shft (member 'shift modifs)) + (ctrl (member 'control modifs)) + (cmd (when (or id notat) + (if (and ctrl shft) (if id "Check" "Locate") + (if shft (if id "About" "Locate") + (if ctrl (if id "Print" "Locate"))))))) + (proof-shell-invisible-command + (format (concat cmd " %s . ") + ;; Notation need to be surrounded by "" + (if id id (concat "\"" notat "\"")))))))) (defun coq-guess-or-ask-for-string (s &optional dontguess) "Asks for a coq identifier with message S. @@ -1211,8 +1206,7 @@ Printing All set." (coq-ask-do-show-all "Show goal number" "Show" t)) ;; Check -(eval-when-compile - (defvar coq-auto-adapt-printing-width)); defpacustom +(defvar coq-auto-adapt-printing-width); defpacustom ;; Since Printing Width is a synchronized option in coq (?) it is retored ;; silently to a previous value when retracting. So we reset the stored width |