diff options
Diffstat (limited to 'doc/sphinx/user-extensions/syntax-extensions.rst')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 4c0e85bdd4..705d67e6c6 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _syntaxextensionsandinterpretationscopes: Syntax extensions and interpretation scopes @@ -378,17 +376,14 @@ for records. Here are examples: Displaying information about notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Printing Notations - - To deactivate the printing of all notations, use the command - ``Unset Printing Notations``. To reactivate it, use the command - ``Set Printing Notations``. +.. flag:: Printing Notations - The default is to use notations for printing terms wherever possible. + Controls whether to use notations for printing terms wherever possible. + Default is on. .. seealso:: - :opt:`Printing All` + :flag:`Printing All` To disable other elements in addition to notations. .. _locating-notations: |