aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-custom.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-08-14 12:48:55 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-08-14 12:48:55 +0000
commit6bf9310b98723952fb40e94aea45c0df3115403c (patch)
treebc93951d5df688849fe1b3bc71001202aa206934 /generic/pg-custom.el
parent94788d76ea579e48ac9bd5d447de24f3c7f5495e (diff)
Add info command to toolbar, and re-enable command, interrupt, restart.
Diffstat (limited to 'generic/pg-custom.el')
-rw-r--r--generic/pg-custom.el7
1 files changed, 4 insertions, 3 deletions
diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index 7445c0e4..ed869229 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -70,9 +70,10 @@ support depends on whether your proof assistant supports it."
(qed "Finish Proof" "Close/save proved theorem" t nil)
(home "Goto Locked End" "Goto end of the last command proceesed" t t)
(find "Find Theorems" "Find theorems" t proof-find-theorems-command)
- (command "Issue Command" "Issue a non-scripting command" nil)
- (interrupt "Interrupt Prover" "Interrupt the proof assistant" t)
- (restart "Restart Scripting" "Restart scripting (clear all locked regions)" t)
+ (info "Identifier Info" "Information about identifier" t proof-query-identifier-command)
+ (command "Issue Command" "Issue a non-scripting command" t t)
+ (interrupt "Interrupt Prover" "Interrupt the proof assistant" t t)
+ (restart "Restart Scripting" "Restart scripting (clear all locked regions)" t t)
(visibility "Toggle Visibility" "Show or hide hidden proofs" nil t)
(help nil "Proof General manual" t t))
"Example value for proof-toolbar-entries. Also used to define scripting menu.