aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
diff options
context:
space:
mode:
authorThéo Zimmermann2020-06-08 13:09:23 +0200
committerThéo Zimmermann2020-06-09 13:32:07 +0200
commitfcbae04dbe2e0777e2901cd4dff3bb5d482e3bc2 (patch)
tree75da1a9dce4d34ba014f8e00cf6b547655c3ce52 /doc/sphinx
parent4642ce1c5924cbfa93d6a8e96cf86839e614623b (diff)
Minor improvements to the section on basics.
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/language/core/basic.rst19
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`).