diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-01-29 09:46:12 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-01-29 09:46:12 +0000 |
| commit | df953a00561ee47fbb2ca09c1985a67f47591fb3 (patch) | |
| tree | ad149186aa219ec39b908798fabf36c1667c3308 | |
| parent | 6a1e043d03eef1f22a681e2d2ac0c181ae7ceee7 (diff) | |
Move proof-experimental-features
| -rw-r--r-- | generic/pg-custom.el | 23 | ||||
| -rw-r--r-- | generic/proof-config.el | 16 |
2 files changed, 23 insertions, 16 deletions
diff --git a/generic/pg-custom.el b/generic/pg-custom.el index 09bcc197..b73ef30e 100644 --- a/generic/pg-custom.el +++ b/generic/pg-custom.el @@ -182,6 +182,29 @@ http://proofgeneral.inf.ed.ac.uk/trac" :type 'file :group 'prover-config) +;;; +;;; Experimental features: not a per-prover settings, +;;; but initialised here because of default value's +;;;; dependency on proof-general-version + +(defcustom proof-experimental-features + (if (string-match "pre" proof-general-version) t) + "*Whether to enable certain features regarded as experimental. +Proof General includes a few features designated as \"experimental\". +Enabling these will usually have no detrimental effects on using PG, +but the features themselves may be buggy. + +We encourage users to set this flag and test the features, but being +aware that the features may be buggy (problem reports and +suggestions for improvements are welcomed). + +In the current 3.7 release, there are no features classed as experimental +so this option is set by default." + :type 'boolean + :group 'proof-user-options) + + + (provide 'pg-custom) ;;; pg-custom.el ends here diff --git a/generic/proof-config.el b/generic/proof-config.el index 45d411a3..047a5d30 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -334,22 +334,6 @@ This is only useful for PG developers." :type 'boolean :group 'proof-user-options) -(defcustom proof-experimental-features - (if (string-match "pre" proof-general-version) t) - "*Whether to enable certain features regarded as experimental. -Proof General includes a few features designated as \"experimental\". -Enabling these will usually have no detrimental effects on using PG, -but the features themselves may be buggy. - -We encourage users to set this flag and test the features, but being -aware that the features may be buggy (problem reports and -suggestions for improvements are welcomed). - -In the current 3.7 release, there are no features classed as experimental -so this option is set by default." - :type 'boolean - :group 'proof-user-options) - ;;; NON BOOLEAN OPTIONS (defcustom proof-follow-mode 'locked |