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.

1 files changed, 9 insertions, 71 deletions

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