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/changelog/03-notations/13965-syndef-principal-scope.rst | 12 ++++++++++++ doc/sphinx/user-extensions/syntax-extensions.rst | 8 ++++++-- doc/tools/docgram/common.edit_mlg | 6 +++--- doc/tools/docgram/fullGrammar | 10 +++------- doc/tools/docgram/orderedGrammar | 4 ++-- 5 files changed, 26 insertions(+), 14 deletions(-) create mode 100644 doc/changelog/03-notations/13965-syndef-principal-scope.rst (limited to 'doc') diff --git a/doc/changelog/03-notations/13965-syndef-principal-scope.rst b/doc/changelog/03-notations/13965-syndef-principal-scope.rst new file mode 100644 index 0000000000..448dbbe3c7 --- /dev/null +++ b/doc/changelog/03-notations/13965-syndef-principal-scope.rst @@ -0,0 +1,12 @@ +- **Added:** + Let the user specify a scope for abbreviation arguments, e.g. + ``Notation abbr X := t (X in scope my_scope)``. + (`#13965 `_, + by Enrico Tassi). +- **Changed:** + The error ``Argument X was previously inferred to be in scope + XXX_scope but is here used in YYY_scope.`` is now the warning + ``[inconsistent-scopes,syntax]`` and can be silenced by + specifying the scope of the argument + (`#13965 `_, + by Enrico Tassi). 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 ` 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 diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index fd1c3c0260..b932fc6e30 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1410,8 +1410,9 @@ syntax_modifier: [ | DELETE "in" "custom" IDENT | REPLACE "in" "custom" IDENT; "at" "level" natural | WITH "in" "custom" IDENT OPT ( "at" "level" natural ) -| REPLACE IDENT; "," LIST1 IDENT SEP "," "at" level -| WITH LIST1 IDENT SEP "," "at" level +| DELETE IDENT; "in" "scope" IDENT +| REPLACE IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ] +| WITH LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ] ] explicit_subentry: [ @@ -2643,7 +2644,6 @@ SPLICE: [ | quoted_attributes (* todo: splice or not? *) | printable | hint -| only_parsing | record_fields | constructor_type | record_binder diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index ab1a9d4c75..47c758b5e8 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1401,18 +1401,13 @@ syntax: [ | "Undelimit" "Scope" IDENT | "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr | "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] -| "Notation" identref LIST0 ident ":=" constr only_parsing +| "Notation" identref LIST0 ident ":=" constr syntax_modifiers | "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] | "Format" "Notation" STRING STRING STRING | "Reserved" "Infix" ne_lstring syntax_modifiers | "Reserved" "Notation" ne_lstring syntax_modifiers ] -only_parsing: [ -| "(" "only" "parsing" ")" -| -] - level: [ | "level" natural | "next" "level" @@ -1428,8 +1423,9 @@ syntax_modifier: [ | "only" "printing" | "only" "parsing" | "format" STRING OPT STRING -| IDENT; "," LIST1 IDENT SEP "," "at" level +| IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ] | IDENT; "at" level OPT binder_interp +| IDENT; "in" "scope" IDENT | IDENT binder_interp | IDENT explicit_subentry ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 5b19b7fc55..b0a7cb91f9 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1096,7 +1096,7 @@ command: [ | "Undelimit" "Scope" scope_name | "Bind" "Scope" scope_name "with" LIST1 class | "Infix" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ] -| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" ) +| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) | "Notation" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ] | "Format" "Notation" string string string | "Reserved" "Infix" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) @@ -1540,7 +1540,7 @@ class: [ syntax_modifier: [ | "at" "level" natural | "in" "custom" ident OPT ( "at" "level" natural ) -| LIST1 ident SEP "," "at" level +| LIST1 ident SEP "," [ "at" level | "in" "scope" ident ] | ident "at" level OPT binder_interp | ident explicit_subentry | ident binder_interp -- cgit v1.2.3