Created
June 14, 2012 11:55
-
-
Save anonymous/2929859 to your computer and use it in GitHub Desktop.
stdin
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
diff --git a/PKGBUILD b/PKGBUILD | |
index 42a6d0f..7645ed8 100644 | |
--- a/PKGBUILD | |
+++ b/PKGBUILD | |
@@ -3,20 +3,23 @@ | |
pkgname=proofgeneral | |
pkgver=4.1 | |
-pkgrel=1 | |
+pkgrel=2 | |
pkgdesc='Generic interface for proof assistants.' | |
arch=('i686' 'x86_64') | |
license=('GPL') | |
url='http://proofgeneral.inf.ed.ac.uk/' | |
depends=('emacs') | |
install="${pkgname}.install" | |
-source=("http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-${pkgver}.tgz") | |
+source=("http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-${pkgver}.tgz" | |
+ "interactive-p.patch") | |
build() { | |
cd ProofGeneral | |
make clean | |
+ patch -p1 < "${srcdir}/interactive-p.patch" | |
+ | |
make | |
} | |
@@ -26,4 +29,5 @@ package() { | |
make PREFIX=${pkgdir}/usr install | |
} | |
-md5sums=('a04ebe2c6b56a4fd6c16a070ea7fe3a9') | |
+md5sums=('a04ebe2c6b56a4fd6c16a070ea7fe3a9' | |
+ '0b58b12f32d01346381fcb5638ebeb08') | |
diff --git a/interactive-p.patch b/interactive-p.patch | |
new file mode 100644 | |
index 0000000..cca0135 | |
--- /dev/null | |
+++ b/interactive-p.patch | |
@@ -0,0 +1,81 @@ | |
+diff --git a/generic/proof-menu.el b/generic/proof-menu.el | |
+index 774b232..0fafdfb 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 9bbd603..d614235 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 41a7966..64b3f72 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 13f12d6..bff072d 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 58a27a9..8533371 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))))) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment