Skip to content

Commit

Permalink
Make introductory paragraphs clearer in summaries
Browse files Browse the repository at this point in the history
Take into account @jfehrle's remarks.
  • Loading branch information
Villetaneuse committed Aug 6, 2024
1 parent c1b6cf4 commit 9dfe019
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 24 deletions.
20 changes: 11 additions & 9 deletions doc/sphinx/language/core/modules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -683,16 +683,18 @@ commands in a module, when outside the module where they were entered. In the
following table:

* a cross (❌) marks an unsupported attribute (compilation error);
* “not available” means that the command has no effect outside the module it was entered;
* “when imported” means that the command has effect outside the module if, and
only if, the module (or the command, via selective importation) is imported;
* “short name when imported” means that the command has effects outside the module;
if the module (or command, via selective importation) is not imported, the
associated identifiers must be qualified;
* “qualified name” means that the command has effects outside the module, but
* “not available” means that the command has no effect outside the :cmd:`Module` it
was entered;
* “when imported” means that the command has effect outside the :cmd:`Module` if, and
only if, the :cmd:`Module` (or the command, via :n:`@filtered_import`) is imported
(with :cmd:`Import` or :cmd:`Export`).
* “short name when imported” means that the command has effects outside the
:cmd:`Module`; if the :cmd:`Module` (or command, via :n:`@filtered_import`) is not
imported, the associated identifiers must be qualified;
* “qualified name” means that the command has effects outside the :cmd:`Module`, but
the corresponding identifier may only be referred to with a qualified name;
* “always” means that the command always has effects outside the module (even if
it is not imported).
* “always” means that the command always has effects outside the :cmd:`Module` (even
if it is not imported).

A similar table for :cmd:`Section` can be found
:ref:`here<visibility-attributes-sections>`.
Expand Down
35 changes: 20 additions & 15 deletions doc/sphinx/language/core/sections.rst
Original file line number Diff line number Diff line change
Expand Up @@ -143,13 +143,13 @@ Summary of locality attributes in a section
-------------------------------------------

This table sums up the effect of locality attributes on the scope of vernacular
commands in a section, when outside the section where they were entered. In the
commands in a :cmd:`Section`, when outside the :cmd:`Section` where they were entered. In the
following table:

* a cross (❌) marks an unsupported attribute (compilation error);
* “not available” means that the command has no effect outside the section it
* “not available” means that the command has no effect outside the :cmd:`Section` it
was entered;
* “available” means that the effects of the command persists outside the section.
* “available” means that the effects of the command persists outside the :cmd:`Section`.
* For :cmd:`Definition` (and :cmd:`Lemma`, ...), :cmd:`Canonical Structure`,
:cmd:`Coercion` and :cmd:`Set` (and :cmd:`Unset`), some locality attributes
will be passed on to the :cmd:`Module` containing the current :cmd:`Section`,
Expand Down Expand Up @@ -245,22 +245,27 @@ A similar table for :cmd:`Module` can be found
module [#note3]_

.. [#note1] For :cmd:`Definition`, :cmd:`Lemma`, ... the default visibility is
to be available outside the section and available with a short name when
imported outside the current module. The :attr:`local` attribute make the
corresponding identifiers available in the current module but only with a
fully qualified name outside the current module.
.. [#note2] For :cmd:`Coercion` and :cmd:`Canonical Structure`, the :attr:`global`
visibility, which is the default, makes them available outside the section,
in the current module, and outside the current module when it is imported.
to be available outside the section and available with a short name when the
current :cmd:`Module` is imported (with :cmd:`Import` or cmd:`Export`)
outside the current :cmd:`Module`.
The :attr:`local` attribute make the corresponding identifiers available in
the current :cmd:`Module` but only with a fully qualified name outside the
current :cmd:`Module`.
.. [#note2] For :cmd:`Coercion` and :cmd:`Canonical Structure`, the
:attr:`global` visibility, which is the default, makes them available outside
the section, in the current :cmd:`Module`, and outside the current
:cmd:`Module` when it is imported (with :cmd:`Import` or cmd:`Export`).
.. [#note3] For :cmd:`Set` and :cmd:`Unset`, the :attr:`export` and
:attr:`global` attributes both make the command's effects persist outside the
current section, in the current module. It will also persist outside the
current module with the :attr:`global` attribute, or with the :attr:`export`
attribute, when the module is imported.
current section, in the current :cmd:`Module`.
It will also persist outside the current :cmd:`Module` with the
:attr:`global` attribute, or with the :attr:`export` attribute, when the
:cmd:`Module` is imported (with :cmd:`Import` or cmd:`Export`).
The default behaviour (no attribute) is to make the setting persist outside
the section in the current module, but not outside the current module.
the section in the current :cmd:`Module`, but not outside the current
:cmd:`Module`.
.. _Admissible-rules-for-global-environments:

Expand Down

0 comments on commit 9dfe019

Please sign in to comment.