diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 35 |
1 files changed, 17 insertions, 18 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index fd315c097d..a28ce600ca 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -267,31 +267,30 @@ The second, more powerful control on printing is by using the format A *format* is an extension of the string denoting the notation with the possible following elements delimited by single quotes: -- extra spaces are translated into simple spaces +- tokens of the form ``'/ '`` are translated into breaking points. If + there is a line break, indents the number of spaces appearing after the + “``/``” (no indentation in the example) -- tokens of the form ``'/ '`` are translated into breaking point, in - case a line break occurs, an indentation of the number of spaces after - the “ ``/``” is applied (2 spaces in the given example) - -- token of the form ``'//'`` force writing on a new line +- tokens of the form ``'//'`` force writing on a new line - well-bracketed pairs of tokens of the form ``'[ '`` and ``']'`` are - translated into printing boxes; in case a line break occurs, an extra - indentation of the number of spaces given after the “ ``[``” is applied - (4 spaces in the example) + translated into printing boxes; if there is a line break, an extra + indentation of the number of spaces after the “``[``” is applied - well-bracketed pairs of tokens of the form ``'[hv '`` and ``']'`` are translated into horizontal-or-else-vertical printing boxes; if the content of the box does not fit on a single line, then every breaking - point forces a newline and an extra indentation of the number of - spaces given after the “ ``[``” is applied at the beginning of each - newline (3 spaces in the example) + point forces a new line and an extra indentation of the number of + spaces after the “``[hv``” is applied at the beginning of each new line - well-bracketed pairs of tokens of the form ``'[v '`` and ``']'`` are translated into vertical printing boxes; every breaking point forces a - newline, even if the line is large enough to display the whole content - of the box, and an extra indentation of the number of spaces given - after the “``[``” is applied at the beginning of each newline + new line, even if the line is large enough to display the whole content + of the box, and an extra indentation of the number of spaces + after the “``[v``” is applied at the beginning of each new line (3 spaces + in the example) + +- extra spaces in other tokens are preserved in the output Notations disappear when a section is closed. No typing of the denoted expression is performed at definition time. Type checking is done only @@ -592,7 +591,7 @@ placeholder being the nesting point. In the innermost occurrence of the nested iterating pattern, the second placeholder is finally filled with the terminating expression. -In the example above, the iterator :math:`φ([~]_E , [~]_I)` is :math:`cons [~]_E [~]_I` +In the example above, the iterator :math:`φ([~]_E , [~]_I)` is :math:`cons [~]_E\, [~]_I` and the terminating expression is ``nil``. Here are other examples: .. coqtop:: in @@ -751,12 +750,12 @@ level is otherwise given explicitly by using the syntax Levels are cumulative: a notation at level ``n`` of which the left end is a term shall use rules at level less than ``n`` to parse this -sub-term. More precisely, it shall use rules at level strictly less +subterm. More precisely, it shall use rules at level strictly less than ``n`` if the rule is declared with ``right associativity`` and rules at level less or equal than ``n`` if the rule is declared with ``left associativity``. Similarly, a notation at level ``n`` of which the right end is a term shall use by default rules at level strictly -less than ``n`` to parse this sub-term if the rule is declared left +less than ``n`` to parse this subterm if the rule is declared left associative and rules at level less or equal than ``n`` if the rule is declared right associative. This is what happens for instance in the rule |