diff options
| author | David Aspinall | 2009-08-07 14:40:17 +0000 |
|---|---|---|
| committer | David Aspinall | 2009-08-07 14:40:17 +0000 |
| commit | b4a8dafffec6c5fc44228760bd227617086581e0 (patch) | |
| tree | 1c1262644e65defd2f0a7692d86071393a6fdbe8 /generic | |
| parent | fcd935b7a2713230349e70f1a13dc6ca0a29fe7c (diff) | |
proof-full-annotation: change default
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 16 |
1 files changed, 2 insertions, 14 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index c71cd350..4a1bfeb7 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -329,18 +329,6 @@ This is only useful for PG developers." :group 'proof-user-options) -(defcustom proof-experimental-features nil - "*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)." - :type 'boolean - :group 'proof-user-options) - ;;; NON BOOLEAN OPTIONS (defcustom proof-follow-mode 'locked @@ -419,10 +407,10 @@ signals to the remote host." :type 'boolean :group 'proof-user-options) -(defcustom proof-full-annotation nil +(defcustom proof-full-annotation t "*Non-nil causes Proof General to add hovers for all proof commands. Proof output is recorded as it occurs interactively; normally if -many steps are taken at once, this output is surpressed. If this +many steps are taken at once, this output is suppressed. If this setting is used to enable it, the proof script will be annotated with full details." :type 'boolean |