Document new Search features.

1 files changed, 32 insertions, 16 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 4149ea7a76..a9a243868f 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -60,6 +60,7 @@ DELETE: [
 | test_only_starredidentrefs
 | test_bracket_ident
 | test_hash_ident
+| test_id_colon
 | test_lpar_id_colon
 | test_lpar_id_coloneq  (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *)
 | test_lpar_id_rpar
@@ -1232,8 +1233,8 @@ query_command: [
 | WITH "SearchPattern" constr_pattern in_or_out_modules
 | REPLACE "SearchRewrite" constr_pattern in_or_out_modules "."
 | WITH "SearchRewrite" constr_pattern in_or_out_modules
-| REPLACE "Search" searchabout_query searchabout_queries "."
-| WITH "Search" searchabout_queries
+| REPLACE "Search" search_query search_queries "."
+| WITH "Search" search_queries
 ]
 
 vernac_toplevel: [
@@ -1458,17 +1459,10 @@ ne_in_or_out_modules: [
 | DELETE "outside" LIST1 global
 ]
 
-searchabout_query: [
-| REPLACE positive_search_mark ne_string OPT scope_delimiter
-| WITH ne_string OPT scope_delimiter
-| REPLACE positive_search_mark constr_pattern
-| WITH constr_pattern
-]
-
-searchabout_queries: [
+search_queries: [
 | DELETE ne_in_or_out_modules
-| REPLACE searchabout_query searchabout_queries
-| WITH LIST1 ( positive_search_mark searchabout_query ) OPT ne_in_or_out_modules
+| REPLACE search_query search_queries
+| WITH LIST1 ( search_query ) OPT ne_in_or_out_modules
 | DELETE (* empty *)
 ]
 
@@ -1476,6 +1470,27 @@ positive_search_mark: [
 | OPTINREF
 ]
 
+SPLICE: [
+| positive_search_mark
+]
+
+search_query: [
+| REPLACE OPT "-" search_item
+| WITH search_item
+| "-" search_query
+| REPLACE OPT "-" "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
+| WITH "[" LIST1 ( LIST1 search_query ) SEP "|" "]"
+]
+
+search_item: [
+| REPLACE search_where ":" ne_string OPT scope_delimiter
+| WITH OPT ( search_where ":" ) ne_string OPT scope_delimiter
+| DELETE ne_string OPT scope_delimiter
+| REPLACE search_where ":" constr_pattern
+| WITH OPT ( search_where ":" ) constr_pattern
+| DELETE constr_pattern
+]
+
 by_notation: [
 | REPLACE ne_string OPT [ "%" IDENT ]
 | WITH ne_string OPT [ "%" scope_key ]
@@ -1631,7 +1646,6 @@ SPLICE: [
 | record_binder
 | at_level_opt
 | table_value
-| positive_search_mark
 | in_or_out_modules
 | option_setting
 | orient
@@ -1665,12 +1679,14 @@ SPLICE: [
 | intropatterns
 | instance_name
 | ne_in_or_out_modules
-| searchabout_queries
+| search_queries
 | locatable
 | scope_delimiter
 | bignat
 | one_import_filter_name
 | register_token
+| search_where
+| extended_def_token
 ] (* end SPLICE *)
 
 RENAME: [
@@ -1719,7 +1735,9 @@ RENAME: [
 | record_binder_body field_body
 | class_rawexpr class
 | smart_global smart_qualid
+(*
 | searchabout_query search_item
+*)
 | option_table setting_name
 | argument_spec_block arg_specs
 | more_implicits_block implicits_alt
@@ -1729,8 +1747,6 @@ RENAME: [
 | numnotoption numeral_modifier
 ]
 
-(* todo: positive_search_mark is a lousy name for OPT "-" *)
-
 (* todo: doesn't work if up above... maybe because 'clause' doesn't exist? *)
 clause_dft_concl: [
 | OPTINREF