diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-08-08 09:41:08 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-08 09:41:08 +0000 |
| commit | 23e09f4733e1c4da88113e931ccb91951161c715 (patch) | |
| tree | 36c2ab8d2ab257349cefa5d0974f7d30fc8f2ae3 | |
| parent | ed90c81cc76fce5b886d9c3e2d5c8a5011d9df91 (diff) | |
Tweak menu; add proof-shell-show-dependency-cmd
| -rw-r--r-- | generic/proof-config.el | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 1a8d2b65..a12ed2e7 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -715,10 +715,10 @@ If a function, it should return the command string to insert." (lockedend "Locked End" nil t) (find "Find Theorems" "Find theorems" t proof-find-theorems-command) - (show "Show Proofs" nil t) - (hide "Hide Proofs" nil t) (command "Issue Command" "Issue a non-scripting command" t) (interrupt "Interrupt Prover" "Interrupt the proof assistant (warning: may break synchronization)" t) + (show "Show Proofs" nil t) + (hide "Hide Proofs" nil t) (info nil "Show online proof assistant information" t proof-info-command) (help nil "Proof General manual" t)) @@ -1931,6 +1931,13 @@ This is an experimental feature, currently work-in-progress." :type '(choice nil regexp) :group 'proof-shell) +(defcustom proof-shell-show-dependency-cmd nil + "Command sent to the prover to display a dependency. +This is typically a command used to print a theorem, constant, or whatever. +A string with %s replaced by the dependency name." + :type 'string + :group 'proof-shell) + (defcustom proof-shell-trace-output-regexp nil "Regexp matching tracing output which should be displayed in trace buffer. Each line which matches this regexp but would otherwise be treated |