From d3963fc6b6dad5a0cf79815f31b2035ca8b3de25 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 19 Mar 2021 14:29:07 +0100
Subject: [abbreviation] allow the user to set arguments scope

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx')

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
-- 
cgit v1.2.3