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