aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-04-07 14:24:47 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-04-07 14:24:47 +0000
commit1d3842f87c31e536efe0c977c70fab478195126d (patch)
tree7bc9e5fe9f95481d8988d24157774c7d4a6f1efd
parenta1cb622759dbfa6e93547e01ff6ad2eb9fc44921 (diff)
Generalisation of proof-info-command to string or fn.
-rw-r--r--generic/proof-config.el11
1 files changed, 6 insertions, 5 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 717705b0..874a53fc 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -648,8 +648,10 @@ Used for Proof General's help menu."
:group 'prover-config)
(defcustom proof-info-command nil
- "Command to ask for help or information in the proof assistant."
- :type 'string
+ "Command to ask for help or information in the proof assistant.
+String or fn. If a string, the command to use.
+If a function, it should return the command string to insert."
+ :type '(choice string function)
:group 'prover-config)
(defcustom proof-showproof-command nil
@@ -674,9 +676,8 @@ If a function, it should return the command string to insert."
:group 'prover-config)
(defcustom proof-find-theorems-command nil
- "Command to search for a theorem containing a given constant. String or fn.
-If a string, the format character `%s' will be replaced by the
-constant name.
+ "Command to search for a theorem containing a given term. String or fn.
+If a string, the format character `%s' will be replaced by the term.
If a function, it should return the command string to insert."
:type '(choice string function)
:group 'prover-config)