diff options
| author | Théo Zimmermann | 2020-06-08 13:09:23 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-06-09 13:32:07 +0200 |
| commit | fcbae04dbe2e0777e2901cd4dff3bb5d482e3bc2 (patch) | |
| tree | 75da1a9dce4d34ba014f8e00cf6b547655c3ce52 | |
| parent | 4642ce1c5924cbfa93d6a8e96cf86839e614623b (diff) | |
Minor improvements to the section on basics.
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index d7f7259ab0..64b29c1c0b 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -417,8 +417,16 @@ more precise description of the scope of these settings): .. FIXME Convert "Extraction Language" to an option. -Flags, options and tables are identified by a series of identifiers, each with an initial -capital letter. +.. insertprodn setting_name setting_name + +.. prodn:: + setting_name ::= {+ @ident } + +.. + + Flags, options and tables are identified by a series of + identifiers. By convention, each of the identifiers start with an + initial capital letter. Flags, options and tables appear in the HTML documentation in blue or gray boxes after the labels "Flag", "Option" and "Table". In the pdf, @@ -428,11 +436,6 @@ they appear after a boldface label. They are listed in the .. cmd:: Set @setting_name {? {| @int | @string } } :name: Set - .. insertprodn setting_name setting_name - - .. prodn:: - setting_name ::= {+ @ident } - If :n:`@setting_name` is a flag, no value may be provided; the flag is set to on. If :n:`@setting_name` is an option, a value of the appropriate type @@ -533,4 +536,4 @@ Newly opened modules and sections inherit the current settings. :cmd:`Unset` commands. If your goal is to define project-wide settings, you should rather use the command-line arguments ``-set`` and ``-unset`` for setting flags and options - (cf. :ref:`command-line-options`). + (see :ref:`command-line-options`). |