diff options
| author | Théo Zimmermann | 2020-05-11 17:41:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-15 18:02:10 +0200 |
| commit | 576d84e4322a9dd7a6d2ffe45172e01182bf44b0 (patch) | |
| tree | 6193c2ce0af15cbe7ed10fd292118c57578c04bc /doc/tools/docgram/common.edit_mlg | |
| parent | 03e0aa5ee57b3b539b0fa34be2e1a02a2803b0be (diff) | |
Update docgram following #12122 and #12229.
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 62cc8ea86b..4149ea7a76 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -59,6 +59,7 @@ DELETE: [ | lookup_at_as_comma | test_only_starredidentrefs | test_bracket_ident +| test_hash_ident | test_lpar_id_colon | test_lpar_id_coloneq (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *) | test_lpar_id_rpar @@ -1485,14 +1486,6 @@ scope_delimiter: [ | WITH "%" scope_key ] -(* Don't show these details *) -DELETE: [ -| register_token -| register_prim_token -| register_type_token -] - - decl_notation: [ | REPLACE ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ] | WITH ne_lstring ":=" constr only_parsing OPT [ ":" scope_name ] @@ -1677,6 +1670,7 @@ SPLICE: [ | scope_delimiter | bignat | one_import_filter_name +| register_token ] (* end SPLICE *) RENAME: [ |