diff options
| author | David Aspinall | 2000-05-01 18:18:30 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-05-01 18:18:30 +0000 |
| commit | e9ac9e8eb3d2567ff1ab12cf7bfdd60d5df2c30f (patch) | |
| tree | 2174f36ab1eb25c86534c6b95177634c11a6f2c2 /doc | |
| parent | e3b0ad751924c57db4ec8e72759edd2070757097 (diff) | |
Added proof-assistant-menu-entries for proof assistant specific menus.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 0083a54c..b2995081 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3534,6 +3534,19 @@ The following variables should be set in the script mode before @code{proof-config-done} is called. These make some settings for the commands and menus available in Proof General. +The first setting controls the proof-assistant specific menu, +if any is defined. + +@c TEXI DOCSTRING MAGIC: proof-assistant-menu-entries +@defvar proof-assistant-menu-entries +Entries for proof assistant specific menu. @* +A list of menu items [@var{name} @var{callback} ENABLE]. See the documentation +of @samp{@code{easy-menu-define}} for more details. +@end defvar + +The remaining settings control the standard commands available +from the generic menu and the toolbar. + @c TEXI DOCSTRING MAGIC: proof-assistant-home-page @defvar proof-assistant-home-page Web address for information on proof assistant.@* @@ -3576,6 +3589,8 @@ If a function, it should return the command string to insert. + + @c defgroup proof-script @node Proof script settings @section Proof script settings |