aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-toolbar.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1999-10-01 11:32:41 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1999-10-01 11:32:41 +0000
commitd0f7e50b70db1b88a561d9277c4bd9151383534f (patch)
treef0cb185d48409a294d97d0d63482b676ddc3a89c /generic/proof-toolbar.el
parent5a135c2193fef3dfbb023d05c56deef77be35847 (diff)
Added interrupt button to toolbar
Diffstat (limited to 'generic/proof-toolbar.el')
-rw-r--r--generic/proof-toolbar.el10
1 files changed, 10 insertions, 0 deletions
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 5c2277a3..3051764d 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -60,6 +60,7 @@
(qed "Finish proof" "Close/save proved theorem" t)
(find "Find theorems" "Find theorems" t)
(command "Issue command" "Issue a non-scripting command" t)
+ (interrupt "Interrupt prover" "Interrupt the proof assistant (warning: may break synchronization)" t)
(info nil "Show proof assistant information" t)
(help nil "Proof General manual" t))
"Example value for proof-toolbar-entries. Also used to define Scripting menu.
@@ -443,6 +444,15 @@ Move point if the end of the locked position is invisible."
(defalias 'proof-toolbar-find 'proof-find-theorems)
+;;
+;; Interrupt button
+;;
+
+(defun proof-toolbar-interrupt-enable-p ()
+ proof-shell-busy)
+
+(defalias 'proof-toolbar-interrupt 'proof-interrupt-process)
+
;;
;; =================================================================