[abbreviation] allow the user to set arguments scope

3 files changed, 8 insertions, 12 deletions

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