aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-config.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-15 22:47:42 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-15 22:47:42 +0000
commit077f1357124a99ea87e666f9074f2966d846e67f (patch)
treeaaa05c43e5c21b9ac9555525c526700310a99144 /generic/proof-config.el
parenta72719e7a1d95d661ceede447295e67479fa8db4 (diff)
proof-shell-interrupts-after-commit: support commit-before-interrupt mode [experimental/temporary].
Diffstat (limited to 'generic/proof-config.el')
-rw-r--r--generic/proof-config.el9
1 files changed, 9 insertions, 0 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el
index c6e073ea..7313502c 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1055,6 +1055,15 @@ See `proof-shell-error-regexp' and `proof-shell-interrupt-regexp'."
:type 'boolean
:group 'proof-shell)
+(defcustom proof-shell-interrupts-after-commit nil
+ "Non-nil means the prover commits changes then checks for interruption.
+
+The default behaviour assumed by Proof General is that interruption
+interrupts the currently executing command and does not commit it.
+Isabelle has changed this since Isabelle2009-1 or thereabouts."
+ :type 'boolean
+ :group 'proof-shell)
+
(defcustom pg-next-error-regexp nil
"Regular expression which matches an error message, perhaps with line/column.
Used by `proof-next-error' to jump to line numbers causing