diff options
| author | David Aspinall | 2004-04-14 12:35:19 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-04-14 12:35:19 +0000 |
| commit | 5221156284124973706bdd2d786c0e7b7114a5a6 (patch) | |
| tree | 667997a7430500d83395c16522d8698d42fdb0b1 | |
| parent | 35280c96fbd05feab780030478b6773f6fa41b87 (diff) | |
Add proof-imenu-enable. Other doc tweaks.
| -rw-r--r-- | generic/proof-config.el | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 6f93e807..5639e278 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -99,8 +99,13 @@ terminator somewhere nearby. Electric!" :group 'proof-user-options) (defcustom proof-toolbar-enable t - "*If non-nil, display Proof General toolbar for script buffers. -NB: the toolbar is only available with XEmacs and GNU Emacs>=21." + "*If non-nil, display Proof General toolbar for script buffers." + :type 'boolean + :set 'proof-set-value + :group 'proof-user-options) + +(defcustom proof-imenu-enable nil + "*If non-nil, display Imenu menu of items for script buffers." :type 'boolean :set 'proof-set-value :group 'proof-user-options) @@ -1015,11 +1020,11 @@ for `proof-script-next-entity-regexps' used for function menus." (defcustom proof-goal-with-hole-regexp nil "Regexp which matches a command used to issue and name a goal. -The name of the theorem is build from the variable +The name of the theorem is built from the variable proof-goal-with-hole-result using the same convention as -query-replace-regexp. +for `query-replace-regexp'. Used for setting names of goal..save regions and for default -function-menu configuration in proof-script-find-next-entity. +configuration of other modes (function menu, imenu). It's safe to leave this setting as nil." :type 'regexp |