aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-config.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1998-10-27 15:18:28 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1998-10-27 15:18:28 +0000
commitfc9af819f6faa4214c376f74a14e4db45178c921 (patch)
tree6505dc2075ca4fa4cdbab9ed2d2f0e5bff502efb /generic/proof-config.el
parent787e3d0cccf840d87111a5626deaeb8c07156a9d (diff)
Moved pbp-goal-command and pbp-hyp-command to proof-config.Moved LEGO specifix.
Diffstat (limited to 'generic/proof-config.el')
-rw-r--r--generic/proof-config.el12
1 files changed, 12 insertions, 0 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el
index bec16319..83b850bf 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -527,6 +527,18 @@ mere warning messages with this regexp)."
:type 'regexp
:group 'proof-shell)
+(defcustom pbp-goal-command nil
+ "Command informing the prover that `pbp-button-action' has been
+ requested on a goal."
+ :type 'regexp
+ :group 'proof-shell)
+
+(defvar pbp-hyp-command nil
+ "Command informing the prover that `pbp-button-action' has been
+ requested on an assumption."
+ :type 'regexp
+ :group 'proof-shell)
+
(defcustom proof-shell-result-start ""
"Regexp matching start of an output from the prover after pbp commands.
In particular, after a `pbp-goal-command' or a `pbp-hyp-command'."