> Find below a first patch.
Is there something else I need to do for this patch to be installed, or
should I just wait a bit more (I have other patches in the pipeline
after this one).
Stefan
> 2018-11-28 Stefan Monnier <monn...@iro.umontreal.ca>
>
> 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.
>
>
>
> 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-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 <d...@dcs.ed.ac.uk>
> ;; Maintainer: Proof General maintainer <proof...@dcs.ed.ac.uk>
> @@ -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,31 +28,10 @@
>
> ;;; 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 <p.c.callag...@durham.ac.uk>
> ;;
> ;; $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
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
