diff options
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index a01f57eb22..5034d9a3c9 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -511,6 +511,12 @@ strategy_flag: [ | OPTINREF ] +filtered_import: [ +| REPLACE global "(" LIST1 one_import_filter_name SEP "," ")" +| WITH global OPT [ "(" LIST1 one_import_filter_name SEP "," ")" ] +| DELETE global +] + functor_app_annot: [ | OPTINREF ] @@ -1582,6 +1588,7 @@ SPLICE: [ | searchabout_queries | locatable | scope_delimiter +| one_import_filter_name ] (* end SPLICE *) RENAME: [ |