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 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- .gitignore | 1 + coq/coq-compile-common.el | 9 +++-- coq/coq-indent.el | 5 ++- coq/coq-local-vars.el | 7 ++-- coq/coq-par-compile.el | 5 ++- coq/coq-seq-compile.el | 5 ++- coq/coq-system.el | 7 ++-- coq/coq.el | 72 +++++++++++++++++++--------------------- generic/pg-goals.el | 8 ++--- generic/pg-response.el | 8 ++--- generic/pg-user.el | 9 +++-- generic/proof-autoloads.el | 2 -- generic/proof-menu.el | 7 ++-- generic/proof-script.el | 8 ++--- generic/proof-shell.el | 10 +++--- generic/proof-site.el | 5 ++- generic/proof-utils.el | 9 ++--- hol-light/hol-light.el | 10 +++--- isar/isabelle-system.el | 5 +-- isar/isar.el | 9 ++--- lib/proof-compat.el | 80 +++++---------------------------------------- obsolete/plastic/plastic.el | 6 ++-- pg-init.el | 25 +++----------- 23 files changed, 110 insertions(+), 202 deletions(-) diff --git a/.gitignore b/.gitignore index 9cd6d703..2039757e 100644 --- a/.gitignore +++ b/.gitignore @@ -2,5 +2,6 @@ nohup.out TAGS ChangeLog +proof-general-autoloads.el *.elc *~ 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 diff --git a/coq/coq.el b/coq/coq.el index 3376f7f3..6b1494a9 100644 --- a/coq/coq.el +++ b/coq/coq.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 @@ -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 diff --git a/generic/pg-goals.el b/generic/pg-goals.el index baab5561..124965e8 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.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 @@ -20,9 +20,9 @@ (eval-when-compile (require 'easymenu) ; easy-menu-add, etc (require 'cl) ; incf - (require 'span) ; span-* - (defvar proof-goals-mode-menu) ; defined by macro below - (defvar proof-assistant-menu)) ; defined by macro in proof-menu + (require 'span)) ; span-* +(defvar proof-goals-mode-menu) ; defined by macro below +(defvar proof-assistant-menu) ; defined by macro in proof-menu (require 'pg-assoc) diff --git a/generic/pg-response.el b/generic/pg-response.el index 43e0e279..650e83a0 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.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,9 @@ (eval-when-compile (require 'easymenu) ; easy-menu-add - (require 'proof-utils) ; deflocal, proof-eval-when-ready-for-assistant - (defvar proof-response-mode-menu nil) - (defvar proof-assistant-menu nil)) + (require 'proof-utils)) ; deflocal, proof-eval-when-ready-for-assistant +(defvar proof-response-mode-menu) +(defvar proof-assistant-menu) (require 'pg-assoc) (require 'span) diff --git a/generic/pg-user.el b/generic/pg-user.el index 126901cb..5a5d6d13 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.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 @@ -863,10 +863,9 @@ The function `substitute-command-keys' is called on the argument." (interactive "e") (if proof-query-identifier-command (save-selected-window - (save-selected-frame - (save-excursion - (mouse-set-point event) - (pg-identifier-near-point-query)))))) + (save-excursion + (mouse-set-point event) + (pg-identifier-near-point-query))))) ;;;###autoload (defun pg-identifier-near-point-query () diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index 083f42f3..5d2a18cd 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -14,8 +14,6 @@ ;;; Code: -(eval-when-compile - (require 'cl)) (eval-when-compile (require 'pg-vars) 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) diff --git a/generic/proof-script.el b/generic/proof-script.el index c938dfad..9c5c06a4 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.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,9 +30,9 @@ (require 'proof-syntax) ; utils for manipulating syntax (eval-when-compile - (require 'easymenu) - (defvar proof-mode-menu nil) - (defvar proof-assistant-menu nil)) + (require 'easymenu)) +(defvar proof-mode-menu) +(defvar proof-assistant-menu) (declare-function proof-shell-strip-output-markup "proof-shell" (string &optional push)) 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)))) diff --git a/generic/proof-site.el b/generic/proof-site.el index e339d022..fd48002f 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.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 @@ -169,8 +169,7 @@ You can use customize to set this variable." (require 'pg-vars) (require 'proof-autoloads) -(eval-when-compile - (defvar Info-dir-contents)) +(defvar Info-dir-contents) ;; Add the info directory to the Info path (if (file-exists-p proof-info-directory) ; for safety diff --git a/generic/proof-utils.el b/generic/proof-utils.el index b4e7e0d1..a2c29824 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.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 @@ -40,7 +40,7 @@ (if (or (not (boundp 'emacs-major-version)) (< emacs-major-version 23) - (string-match "XEmacs" emacs-version)) + (featurep 'xemacs)) (error "Proof General is not compatible with Emacs %s" emacs-version)) (unless (equal pg-compiled-for (pg-emacs-version-cookie)) @@ -399,8 +399,9 @@ or if the window is the only window of its frame." (select-window window)))) ;; the window is the full width, right? ;; [if not, we may be in horiz-split scheme, problematic] - (not (window-leftmost-p window)) - (not (window-rightmost-p window))) + (not (zerop (car (window-edges window)))) ;not leftmost + (not (>= (nth 2 (window-edges window)) ;not rightmost + (frame-width (window-frame window))))) ;; OK, we're not going to adjust the height here. Moreover, ;; we'll make sure the height can be changed elsewhere. (setq window-size-fixed nil) diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index 2b4f3989..808e04a9 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.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,12 +22,10 @@ (require 'proof-easy-config) ; easy configure mechanism (require 'proof-syntax) ; functions for making regexps -(or (proof-try-require 'caml-font) ; use OCaml Emacs mode syntax - (defvar caml-font-lock-keywords nil)) ; +(proof-try-require 'caml-font) ; use OCaml Emacs mode syntax (eval-when-compile - (require 'proof-tree) - (defvar caml-font-lock-keywords nil)) + (require 'proof-tree)) (defcustom hol-light-home (or (getenv "HOLLIGHT_HOME") @@ -317,7 +315,7 @@ You need to restart Emacs if you change this setting." proof-script-font-lock-keywords (append - caml-font-lock-keywords + (bound-and-true-p caml-font-lock-keywords) (list (cons (proof-ids-to-regexp hol-light-keywords) 'font-lock-keyword-face) (cons (proof-ids-to-regexp hol-light-tactics) 'proof-tactics-name-face) diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el index e399474b..0b61aab0 100644 --- a/isar/isabelle-system.el +++ b/isar/isabelle-system.el @@ -1,6 +1,7 @@ ;; isabelle-system.el --- Interface with Isabelle system ;; ;; Copyright (C) 2000 LFCS Edinburgh, David Aspinall. +;; Copyright (C) 2018 Free Software Foundation, Inc. ;; ;; Author: David Aspinall ;; Maintainer: Proof General maintainer @@ -20,8 +21,8 @@ (require 'scomint) (require 'proof-site) (require 'proof-menu) - (require 'proof-syntax) - (defvar proof-assistant-menu)) + (require 'proof-syntax)) +(defvar proof-assistant-menu) (declare-function mapcan "cl-extra") ; spurious bytecomp warning diff --git a/isar/isar.el b/isar/isar.el index bb755d4f..917f8f6a 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -1,6 +1,7 @@ ;; isar.el --- Major mode for Isabelle/Isar proof assistant ;; ;; Copyright (C) 1994-2010 LFCS Edinburgh. +;; Copyright (C) 2018 Free Software Foundation, Inc. ;; ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; @@ -24,10 +25,10 @@ (require 'proof-syntax) (require 'pg-goals) (require 'pg-vars) - (require 'outline) - (defvar comment-quote-nested) - (defvar isar-use-find-theorems-form) - (defvar isar-use-linear-undo)) + (require 'outline)) +(defvar comment-quote-nested) +(defvar isar-use-find-theorems-form) +(defvar isar-use-linear-undo) (require 'proof) (require 'isabelle-system) ; system code diff --git a/lib/proof-compat.el b/lib/proof-compat.el index abbdb465..25c029c6 100644 --- a/lib/proof-compat.el +++ b/lib/proof-compat.el @@ -1,9 +1,9 @@ -;;; proof-compat.el --- Operating system and Emacs version compatibility +;;; proof-compat.el --- Operating system and Emacs version compatibility -*- 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 @@ -28,29 +28,8 @@ ;;; Code: -(require 'easymenu) (require 'cl) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; -;;; Architecture flags -;;; - -;; can use eval-and-compile to allow optimisation, but that would -;; require recompilation for Windows -(defvar proof-running-on-win32 (memq system-type '(win32 windows-nt cygwin)) - "Non-nil if Proof General is running on a windows variant system.") - - -;; Workaround a small bug in Carbon Emacs Winter 2008 (at least) -;; Menu presses query this variable, but it's not bound unless -;; mode engaged. Not noticeable in normal use, but it is as soon -;; as debug-on-error is engaged. -(with-no-warnings - (if (and (boundp 'carbon-emacs-package-version) - (not (boundp 'mac-key-mode))) - (setq mac-key-mode nil))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; ;;; Modifications and adjustments @@ -64,8 +43,8 @@ Done by removing all properties mentioned by custom library. The symbol itself is left defined, in case it has been changed in the current Emacs session." - (mapc (lambda (prop) (remprop symbol prop)) - '(default + (dolist (prop + '(default standard-value force-value variable-comment @@ -83,49 +62,8 @@ in the current Emacs session." custom-version saved-value theme-value - theme-face))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; -;;; GNU Emacs compatibility with XEmacs -;;; - -(unless (fboundp 'save-selected-frame) -(defmacro save-selected-frame (&rest body) - "Execute forms in BODY, then restore the selected frame. -The value returned is the value of the last form in BODY." - (let ((old-frame (gensym "ssf"))) - `(let ((,old-frame (selected-frame))) - (unwind-protect - (progn ,@body) - (select-frame ,old-frame)))))) - -;; These functions are used in the intricate logic around -;; shrink-to-fit. - -;; window-leftmost-p, window-rightmost-p: my implementations -(or (fboundp 'window-leftmost-p) - (defun window-leftmost-p (window) - (zerop (car (window-edges window))))) - -(or (fboundp 'window-rightmost-p) - (defun window-rightmost-p (window) - (>= (nth 2 (window-edges window)) - (frame-width (window-frame window))))) - -(or (fboundp 'window-bottom-p) - (defun window-bottom-p (window) - (>= (nth 3 (window-edges window)) - (frame-height (window-frame window))))) - -;; find-coding-system emulation for GNU Emacs -(unless (fboundp 'find-coding-system) - (defun find-coding-system (name) - "Retrieve the coding system of the given name, or nil if non-such." - (condition-case nil - (check-coding-system name) - (error nil)))) + theme-face)) + (remprop symbol prop))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -137,9 +75,9 @@ The value returned is the value of the last form in BODY." ;; makes every suffix be added as a completion! (eval-after-load "completion" -'(defun completion-before-command () - (if (and (symbolp this-command) (get this-command 'completion-function)) - (funcall (get this-command 'completion-function))))) + '(defun completion-before-command () + (if (and (symbolp this-command) (get this-command 'completion-function)) + (funcall (get this-command 'completion-function))))) (provide 'proof-compat) ;;; proof-compat.el ends here diff --git a/obsolete/plastic/plastic.el b/obsolete/plastic/plastic.el index f5462ba6..09a61b27 100644 --- a/obsolete/plastic/plastic.el +++ b/obsolete/plastic/plastic.el @@ -1,5 +1,7 @@ ;; plastic.el - Major mode for Plastic proof assistant ;; +;; Portions © Copyright 2018 Free Software Foundation, Inc. +;; ;; Author: Paul Callaghan ;; ;; $Id$ @@ -15,8 +17,8 @@ (require 'cl) (require 'span) (require 'proof-syntax) - (require 'outline) - (defvar plastic-keymap nil)) + (require 'outline)) +(defvar plastic-keymap) ;FIXME: Not defined anywhere! (require 'plastic-syntax) diff --git a/pg-init.el b/pg-init.el index a6405361..3a2e5492 100644 --- a/pg-init.el +++ b/pg-init.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 @@ -42,25 +42,10 @@ ;;; Code: ;;;###autoload -(eval-and-compile - (defvar pg-init--script-full-path - (or (and load-in-progress load-file-name) - (bound-and-true-p byte-compile-current-file) - (buffer-file-name))) - (defvar pg-init--pg-root - (file-name-directory pg-init--script-full-path))) - -;;;###autoload -(unless (bound-and-true-p byte-compile-current-file) - ;; This require breaks compilation, so it must only run when loading the package. - (require 'proof-site (expand-file-name "generic/proof-site" pg-init--pg-root))) - -(eval-when-compile - (let ((byte-compile-directories - '("generic" "lib" - "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox"))) - (dolist (dir byte-compile-directories) - (add-to-list 'load-path (expand-file-name dir pg-init--pg-root))))) +(if t (require 'proof-site + (expand-file-name "generic/proof-site" + (file-name-directory + (or load-file-name buffer-file-name))))) (provide 'pg-init) ;;; pg-init.el ends here -- cgit v1.2.3