diff options
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 fe166524bf..b5a234a86a 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1400,18 +1400,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" @@ -1427,8 +1422,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 ] |