diff options
| author | Enrico Tassi | 2021-03-19 14:29:07 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-04-07 19:59:46 +0200 |
| commit | d3963fc6b6dad5a0cf79815f31b2035ca8b3de25 (patch) | |
| tree | 2ba6b35deb5f7ba096662205a99fb942455ef878 /doc/sphinx | |
| parent | eec8ba3a0e807e8de038eb0feaf5db003f423e62 (diff) | |
[abbreviation] allow the user to set arguments scope
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 453e878a5d..0db9d0a862 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1181,7 +1181,7 @@ Here are the syntax elements used by the various notation commands. .. prodn:: syntax_modifier ::= at level @natural | in custom @ident {? at level @natural } - | {+, @ident } at @level + | {+, @ident } {| at @level | in scope @ident } | @ident at @level {? @binder_interp } | @ident @explicit_subentry | @ident @binder_interp @@ -1373,6 +1373,10 @@ interpreted in the scope stack extended with the scope bound to :n:`@scope_key`. Removes the delimiting keys associated with a scope. +The arguments of an :ref:`abbreviation <Abbreviations>` can be interpreted +in a scope stack locally extended with a given scope by using the modifier +:n:`{+, @ident } in scope @scope_name`.s + Binding types or coercion classes to a notation scope ++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -1566,7 +1570,7 @@ Displaying information about scopes Abbreviations -------------- -.. cmd:: Notation @ident {* @ident__parm } := @one_term {? ( only parsing ) } +.. cmd:: Notation @ident {* @ident__parm } := @one_term {? ( {+, @syntax_modifier } ) } :name: Notation (abbreviation) .. todo: for some reason, Sphinx doesn't complain about a duplicate name if |