> I'm happy to push it for you. Would you mind sending a copy as a `git
> format-patch` attachment, so that the commit is properly attributed?
Here it is,
Stefan
>From 1cd25fa20ccac27835b1609cfc089615aade2575 Mon Sep 17 00:00:00 2001
From: Stefan Monnier <monn...@iro.umontreal.ca>
Date: Tue, 11 Dec 2018 18:48:51 -0500
Subject: [PATCH] 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 <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,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 <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
--
2.19.2
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
