9 files changed, 30 insertions, 36 deletions
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)