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/tools/docgram/orderedGrammar | |
| parent | eec8ba3a0e807e8de038eb0feaf5db003f423e62 (diff) | |
[abbreviation] allow the user to set arguments scope
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 4 |
1 files changed, 2 insertions, 2 deletions
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 |