diff options
| author | Thomas Kleymann | 1998-10-30 16:34:38 +0000 |
|---|---|---|
| committer | Thomas Kleymann | 1998-10-30 16:34:38 +0000 |
| commit | 00c337af2ea574baf01a26581b80aa1fd955e2f0 (patch) | |
| tree | bc522ddcd85ecae4f3db4fc007dc22b771d9591c /generic/proof-config.el | |
| parent | 4159c005b516ea482b6d0e5fc5e1d960348383c4 (diff) | |
implemented new buffer model. The goals buffer is now exclusively
reserved for goals.
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 28 |
1 files changed, 21 insertions, 7 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index b4f42458..9fcb13ec 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -198,6 +198,11 @@ Could come either from proof assistant or Proof General itself." ;; functions. This is why prover-config appears under the ;; proof-general-internal group. +(defcustom proof-assistant-home-page "http://www.dcs.ed.ac.uk/home/proofgen/" + "Web address of the proof assistant Proof General is using." + :type 'string + :group 'prover-config) + (defcustom proof-assistant "" "Name of the proof assistant Proof General is using. This is set automatically by the mode stub defined in proof-site, @@ -212,29 +217,38 @@ from the name given in proof-assistant-table." ;; 2. The major modes used by Proof General. ;; -;; FIXME: these symbols could be set automatically to standard values, +;; FIXME: these functions could be set automatically to standard values, ;; i.e. <assistant>-mode, <assistant>-shell-mode, <assistant>-pbp-mode. ;; FIXME: mode-for-script is unused at the moment, added just for ;; uniformity. The other two are used when a shell buffer is started. -(defcustom proof-mode-for-shell nil +(defcustom proof-mode-for-shell 'proof-shell-mode "Mode for proof shell buffers. +Usually customised for specific prover. +Suggestion: this can be set in proof-pre-shell-start-hook." + :type 'function + :group 'prover-config) + +(defcustom proof-mode-for-response 'proof-response-mode + "Mode for proof response buffer. +Usually customised for specific prover. Suggestion: this can be set in proof-pre-shell-start-hook." - :type 'symbol + :type 'function :group 'prover-config) -(defcustom proof-mode-for-pbp nil +(defcustom proof-mode-for-pbp 'pbp-mode "Mode for proof state display buffers. +Usually customised for specific prover. Suggestion: this can be set in proof-pre-shell-start-hook." - :type 'symbol + :type 'function :group 'prover-config) -(defcustom proof-mode-for-script nil +(defcustom proof-mode-for-script 'ignore "Mode for proof script buffers. This is used by Proof General to find out which buffers contain proof scripts. Suggestion: this can be set in the script mode configuration." - :type 'symbol + :type 'function :group 'prover-config) |