diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 3ca1dda4d6..edec13f681 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -840,10 +840,11 @@ gives a way to let any arbitrary expression which is not handled by the custom entry ``expr`` be parsed or printed by the main grammar of term up to the insertion of a pair of curly brackets. -.. cmd:: Print Grammar @ident. +.. cmd:: Print Custom Grammar @ident. + :name: Print Custom Grammar - This displays the state of the grammar for terms and grammar for - patterns associated to the custom entry :token:`ident`. + This displays the state of the grammar for terms associated to + the custom entry :token:`ident`. Summary ~~~~~~~ @@ -1376,6 +1377,8 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. +.. _numeral-notations: + Numeral notations ----------------- |