It appears that proof-general won't compile with emacs 24, due to calls to interactive-p. The replaccement is called-interactively-p, which was introduced in emacs 22. ---
I am not sure that 'any is the right argument to be passing to called-interactively-p (instead of 'interactive), although the documentation suggests the the latter should rarely be used. On Sun, 09 Oct 2011 09:44:48 +0000, bugzilla-dae...@gentoo.org wrote: > https://bugs.gentoo.org/show_bug.cgi?id=386465 > > --- Comment #1 from Ulrich Müller <u...@gentoo.org> 2011-10-09 09:44:48 UTC > --- > Unfortunately, byte-compilation fails with the latest Emacs 24 pretest > (emacs-vcs-24.0.90): > > emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar > (lambda > (d) (concat > "/var/tmp/portage/app-emacs/proofgeneral-4.1/work/ProofGeneral-4.1/" > (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego pgshell phox generic > lib > ))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote > mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq > byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) > byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f > batch-byte-compile isar/isabelle-system.el > > In toplevel form: > isar/isabelle-system.el:295:16:Error: `interactive-p' is an obsolete function > (as of Emacs 23.2); use `called-interactively-p' instead. > make[1]: *** [isar/isabelle-system.elc] Error 1 > make[1]: Leaving directory > `/var/tmp/portage/app-emacs/proofgeneral-4.1/work/ProofGeneral-4.1' > make: *** [compile] Error 2 > emake failed > > > I'd rather like to have this problem fixed before doing the version bump. > Could > you report it upstream please? generic/proof-menu.el | 2 +- generic/proof-script.el | 6 +++--- generic/proof-splash.el | 2 +- isar/isabelle-system.el | 2 +- lib/scomint.el | 2 +- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 89f148f..143b9c1 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -49,7 +49,7 @@ without adjusting window layout." ;; trace buffer, etc. (Makes less sense from the menu, though, ;; where it seems more natural just to rotate from last position) (cond - ((and (interactive-p) + ((and (called-interactively-p 'any) (eq last-command 'proof-display-some-buffers)) (incf proof-display-some-buffers-count)) (t diff --git a/generic/proof-script.el b/generic/proof-script.el index abf966d..95f53ec 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -431,13 +431,13 @@ Point must be after the locked region or this will signal an error." If called interactively or SWITCH is non-nil, switch to script buffer. If called interactively, a mark is set at the current location with `push-mark'" (interactive) - (if (and proof-script-buffer (interactive-p)) + (if (and proof-script-buffer (called-interactively-p 'any)) (push-mark)) (proof-with-script-buffer (if ;; there is an active scripting buffer and it's not displayed (and proof-script-buffer (not (get-buffer-window proof-script-buffer)) - (or switch (interactive-p))) + (or switch (called-interactively-p 'any))) ;; display it (switch-to-buffer proof-script-buffer)) (goto-char (proof-unprocessed-begin)))) @@ -1260,7 +1260,7 @@ activation is considered to have failed and an error is given." ;; immediately because scripting has been turned on now. (if proof-activate-scripting-hook (let - ((activated-interactively (interactive-p))) + ((activated-interactively (called-interactively-p 'any))) (setq proof-shell-last-output-kind nil) (run-hooks 'proof-activate-scripting-hook) ;; If activate scripting functions caused an error, diff --git a/generic/proof-splash.el b/generic/proof-splash.el index 9a979a5..ebd4cab 100644 --- a/generic/proof-splash.el +++ b/generic/proof-splash.el @@ -287,7 +287,7 @@ binding to remove this buffer." (progn ;; disable ordinary emacs splash (setq inhibit-startup-message t) - (proof-splash-display-screen (not (interactive-p)))) + (proof-splash-display-screen (not (called-interactively-p 'any)))) ;; Otherwise, a message (message "Welcome to %s Proof General!" proof-assistant)) (setq proof-splash-seen t))) diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el index ea6879c..4d2b9cc 100644 --- a/isar/isabelle-system.el +++ b/isar/isabelle-system.el @@ -292,7 +292,7 @@ for you, you should disable this behaviour." "Refresh isabelle-logics-menu-entries, returning new entries." (interactive) (if (and isabelle-refresh-logics - (or isabelle-time-to-refresh-logics (interactive-p))) + (or isabelle-time-to-refresh-logics (called-interactively-p 'any))) (progn (setq isabelle-logics-available (isa-tool-list-logics)) (isabelle-logics-menu-calculate) diff --git a/lib/scomint.el b/lib/scomint.el index 641a152..1290ab6 100644 --- a/lib/scomint.el +++ b/lib/scomint.el @@ -251,7 +251,7 @@ NO-NEWLINE is non-nil." (save-excursion (condition-case nil (goto-char - (if (interactive-p) scomint-last-input-end scomint-last-output-start)) + (if (called-interactively-p 'any) scomint-last-input-end scomint-last-output-start)) (error nil)) (while (re-search-forward "\r+$" pmark t) (replace-match "" t t))))) -- 1.7.6.1 _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
