From 70dfbc54d9a6b559dbfcfd6105a7e8c80d78d888 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 26 Feb 2017 00:28:18 -0500 Subject: Fix incorrect assumption that noninteractive == byte-compiling The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't. --- generic/pg-user.el | 4 ++-- generic/proof-splash.el | 2 +- generic/proof-useropts.el | 1 + generic/proof.el | 2 +- 4 files changed, 5 insertions(+), 4 deletions(-) (limited to 'generic') diff --git a/generic/pg-user.el b/generic/pg-user.el index 513b477b..effe1eb5 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -563,9 +563,9 @@ last use time, to discourage saving these into the users database." ;; NB: completion table is expected to be set when proof-script ;; is loaded! Call `proof-script-add-completions' to update. -(unless noninteractive ; during compilation +(unless (bound-and-true-p byte-compile-current-file) (eval-after-load "completion" - '(proof-add-completions))) + '(proof-add-completions))) (defun proof-script-complete (&optional arg) "Like `complete' but case-fold-search set to proof-case-fold-search." diff --git a/generic/proof-splash.el b/generic/proof-splash.el index 25db0946..7e7b8d54 100644 --- a/generic/proof-splash.el +++ b/generic/proof-splash.el @@ -264,7 +264,7 @@ binding to remove this buffer." (defun proof-splash-message () "Make sure the user gets welcomed one way or another." (interactive) - (unless (or proof-splash-seen noninteractive) + (unless (or proof-splash-seen noninteractive (bound-and-true-p byte-compile-current-file)) (if proof-splash-enable (progn ;; disable ordinary emacs splash diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index b2cbb97a..eb9942a7 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -43,6 +43,7 @@ approximation we test whether proof-config is fully-loaded yet." (set-default sym value) (when (and (not noninteractive) + (not (bound-and-true-p byte-compile-current-file)) (featurep 'pg-custom) (featurep 'proof-config)) (if (fboundp sym) diff --git a/generic/proof.el b/generic/proof.el index 1acfae71..4e7ddbea 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -26,7 +26,7 @@ (require 'proof-site) ; site/prover config, global vars, autoloads -(unless noninteractive +(unless (or noninteractive (bound-and-true-p byte-compile-current-file)) (proof-splash-message)) ; welcome the user now. (require 'proof-compat) ; Emacs and OS compatibility -- cgit v1.2.3 From 33614d35a25b54c23171c360a61b913f0c1158ce Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 25 Feb 2017 19:06:26 -0500 Subject: Fix incorrect uses of defvar It didn't really matter that these variables were defined and set to nil during compilation, since we ran compilation in a clean Emacs in --batch mode; it does matter now, however, since package.el compiles PG in the user's currently running Emacs instance. --- generic/pg-pamacs.el | 2 +- generic/proof-menu.el | 16 +++------------- generic/proof-site.el | 2 +- 3 files changed, 5 insertions(+), 15 deletions(-) (limited to 'generic') diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el index 4958b360..4bc61c15 100644 --- a/generic/pg-pamacs.el +++ b/generic/pg-pamacs.el @@ -260,7 +260,7 @@ This macro also extends the `proof-assistant-settings' list." (eval-when-compile (if (boundp 'proof-assistant-symbol) ;; declare variable to compiler to prevent warnings - (eval `(defvar ,(proof-ass-sym name) nil "Dummy for compilation.")))) + (eval `(defvar ,(proof-ass-sym name))))) `(proof-defpacustom-fn (quote ,name) (quote ,val) (quote ,args))) diff --git a/generic/proof-menu.el b/generic/proof-menu.el index df617347..f029afcb 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -10,23 +10,13 @@ (require 'cl) ; mapcan ;;; Code: -(eval-when (compile) - (defvar proof-assistant-menu nil) ; defined by macro in proof-menu-define-specific - (defvar proof-mode-map nil)) - -(require 'proof-utils) ; proof-deftoggle, proof-eval-when-ready-for-assistant -(require 'proof-useropts) -(require 'proof-config) - - - - - (eval-when-compile (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) +(require 'proof-config) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; diff --git a/generic/proof-site.el b/generic/proof-site.el index 671c3c82..17ca325c 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -163,7 +163,7 @@ You can use customize to set this variable." (require 'proof-autoloads) (eval-when-compile - (defvar Info-dir-contents nil)) + (defvar Info-dir-contents)) ;; Add the info directory to the Info path (if (file-exists-p proof-info-directory) ; for safety -- cgit v1.2.3 From 5b85cc7793fbedd656d118454682e43d71dd05dc Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 25 Feb 2017 19:09:32 -0500 Subject: Remove some Emacs <24.1 compatibility cruft --- generic/pg-response.el | 46 ++++++++++++++++------------------------------ 1 file changed, 16 insertions(+), 30 deletions(-) (limited to 'generic') diff --git a/generic/pg-response.el b/generic/pg-response.el index 893d1f6f..8b6a413a 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -99,33 +99,21 @@ Internal variable, setting this will have no effect!") "List of GNU Emacs frame parameters for secondary frames.") (defun proof-multiple-frames-enable () - ; special-display-regexps is obsolete, let us let it for a while and - ; remove it later - (unless (eval-when-compile (boundp 'display-buffer-alist)) - (let ((spdres (cons - pg-response-special-display-regexp - proof-multiframe-parameters))) - (if proof-multiple-frames-enable - (add-to-list 'special-display-regexps spdres) - (setq special-display-regexps - (delete spdres special-display-regexps))))) - ; This is the current way to do it - (when (eval-when-compile (boundp 'display-buffer-alist)) - (let - ((display-buffer-entry - (cons pg-response-special-display-regexp - `((display-buffer-reuse-window display-buffer-pop-up-frame) . - ((reusable-frames . t) - (pop-up-frame-parameters - . - ,proof-multiframe-parameters)))))) - (if proof-multiple-frames-enable - (add-to-list - 'display-buffer-alist - display-buffer-entry) - ;(add-to-list 'display-buffer-alist (proof-buffer-dislay)) - (setq display-buffer-alist - (delete display-buffer-entry display-buffer-alist))))) + (let + ((display-buffer-entry + (cons pg-response-special-display-regexp + `((display-buffer-reuse-window display-buffer-pop-up-frame) . + ((reusable-frames . t) + (pop-up-frame-parameters + . + ,proof-multiframe-parameters)))))) + (if proof-multiple-frames-enable + (add-to-list + 'display-buffer-alist + display-buffer-entry) + ;(add-to-list 'display-buffer-alist (proof-buffer-dislay)) + (setq display-buffer-alist + (delete display-buffer-entry display-buffer-alist)))) (proof-layout-windows)) (defun proof-three-window-enable () @@ -521,9 +509,7 @@ and start at the first error." ;; Pop up a window. (display-buffer proof-response-buffer - (and (eval-when-compile - (boundp 'display-buffer-alist)) - proof-multiple-frames-enable + (and proof-multiple-frames-enable (cons nil proof-multiframe-parameters)))))) ;; Make sure the response buffer stays where it is, ;; and make sure source buffer is visible -- cgit v1.2.3 From 673082b2bee3ca327db56bdc559f7f925259d1c8 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 25 Feb 2017 19:18:16 -0500 Subject: Remove unnecessary calls to 'eval-and-compile' --- generic/pg-assoc.el | 13 ++++++------- generic/proof-shell.el | 1 - 2 files changed, 6 insertions(+), 8 deletions(-) (limited to 'generic') diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el index 6a27cd29..a8a52099 100644 --- a/generic/pg-assoc.el +++ b/generic/pg-assoc.el @@ -16,13 +16,12 @@ (require 'proof-utils) -(eval-and-compile ; defines proof-universal-keys-only-mode-map at compile time - (define-derived-mode proof-universal-keys-only-mode fundamental-mode - proof-general-name "Universal keymaps only" - ;; Doesn't seem to supress TAB, RET - (suppress-keymap proof-universal-keys-only-mode-map 'all) - (proof-define-keys proof-universal-keys-only-mode-map - proof-universal-keys))) +(define-derived-mode proof-universal-keys-only-mode fundamental-mode + proof-general-name "Universal keymaps only" + ;; Doesn't seem to supress TAB, RET + (suppress-keymap proof-universal-keys-only-mode-map 'all) + (proof-define-keys proof-universal-keys-only-mode-map + proof-universal-keys)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 51305eef..93f1bbef 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1911,7 +1911,6 @@ Error messages are displayed as usual." ;; Proof General shell mode definition ;; -;(eval-and-compile ; to define vars ;;;###autoload (define-derived-mode proof-shell-mode scomint-mode "proof-shell" "Proof General shell mode class for proof assistant processes" -- cgit v1.2.3 From 98f2e463287e3562dc7b7126e062919a8604ca4a Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 25 Feb 2017 19:35:35 -0500 Subject: Remove compile-time calls to proof-ready-for-assistant Compilation used to run in a separate Emacs process for each file, but that's not what happens when installing PG with package.el. --- generic/pg-pamacs.el | 4 ---- 1 file changed, 4 deletions(-) (limited to 'generic') diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el index 4bc61c15..8b9b83c7 100644 --- a/generic/pg-pamacs.el +++ b/generic/pg-pamacs.el @@ -257,10 +257,6 @@ Additional properties in the ARGS prop list may include: askprefs message. This macro also extends the `proof-assistant-settings' list." - (eval-when-compile - (if (boundp 'proof-assistant-symbol) - ;; declare variable to compiler to prevent warnings - (eval `(defvar ,(proof-ass-sym name))))) `(proof-defpacustom-fn (quote ,name) (quote ,val) (quote ,args))) -- cgit v1.2.3 From d3170a0cbe470cd620bc16e04eb148e554047d35 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 25 Feb 2017 20:15:09 -0500 Subject: Remove uses of defpgdefault in coq-abbrev This file is `require'-d when compiling coq.el, and at that point the proof assistant isn't set to coq yet, so it would define variables prefixed by `nil-' instead of `coq'. --- generic/pg-pamacs.el | 2 ++ 1 file changed, 2 insertions(+) (limited to 'generic') diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el index 8b9b83c7..d7bb1bf3 100644 --- a/generic/pg-pamacs.el +++ b/generic/pg-pamacs.el @@ -155,6 +155,8 @@ Usage: (defpgdefault SYM VALUE)" ;;;###autoload (defun proof-defpacustom-fn (name val args) "As for macro `defpacustom' but evaluating arguments." + (unless (and proof-assistant (not (string= proof-assistant ""))) + (error "No proof assistant defined")) (let (newargs setting evalform type descr) (while args (cond -- cgit v1.2.3