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.

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 <da@dcs.ed.ac.uk>
 ;; Maintainer:  Proof General maintainer <proofgen@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.Callaghan@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