diff options
author | David Aspinall <da@inf.ed.ac.uk> | 1998-10-27 15:18:28 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 1998-10-27 15:18:28 +0000 |
commit | fc9af819f6faa4214c376f74a14e4db45178c921 (patch) | |
tree | 6505dc2075ca4fa4cdbab9ed2d2f0e5bff502efb /generic/proof-config.el | |
parent | 787e3d0cccf840d87111a5626deaeb8c07156a9d (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.el | 12 |
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'." |