diff options
| author | Jim Fehrle | 2018-09-01 12:39:09 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-09-20 18:27:08 -0700 |
| commit | ec7dd674ea25dfd36c007bb863fed63ce8d31ff2 (patch) | |
| tree | 2f73dd477ac9276ba8ed9409aab613370d29c7fb /doc/sphinx/user-extensions/syntax-extensions.rst | |
| parent | d4b5de427d94d82f09d58e0f1095f052a5900914 (diff) | |
Rewrite "Flags, Options and Tables" section.
Mark boolean-valued options with :flag:
Adjust tactic and command names so parameters aren't shown in the index unless
they're needed for disambiguation.
Remove references to synchronous options.
Revise doc for tables.
Correct indentation for text below :flag:
Diffstat (limited to 'doc/sphinx/user-extensions/syntax-extensions.rst')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 0236f19490..705d67e6c6 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -376,17 +376,14 @@ for records. Here are examples: Displaying information about notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. opt:: Printing Notations +.. flag:: Printing Notations - To deactivate the printing of all notations, use the command - ``Unset Printing Notations``. To reactivate it, use the command - ``Set 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: |