Merge PR #11961: Convert vernac commands chapter to prodn, update syntax

Ack-by: Zimmi48
Ack-by: cpitclaudel

3 files changed, 220 insertions, 150 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 60b845c4be..a01f57eb22 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -151,8 +151,7 @@ fields: [ | DELETENT ]
 
 dirpath: [
 | REPLACE ident LIST0 field
-| WITH ident
-| dirpath field_ident
+| WITH LIST0 ( ident "." ) ident
 ]
 
 binders: [
@@ -220,6 +219,15 @@ tactic_expr0: [
 | WITH "[>" tactic_then_gen "]"
 ]
 
+(* lexer token *)
+IDENT: [
+| ident
+]
+
+scope: [
+| IDENT
+]
+
 operconstr100: [
 | MOVETO term_cast operconstr99 "<:" operconstr200
 | MOVETO term_cast operconstr99 "<<:" operconstr200
@@ -240,7 +248,9 @@ operconstr9: [
 
 operconstr1: [
 | REPLACE operconstr0 ".(" global LIST0 appl_arg ")"
-| WITH operconstr0 ".(" global LIST0 appl_arg ")"
+| WITH    operconstr0 ".(" global LIST0 appl_arg ")" (* huh? *)
+| REPLACE operconstr0 "%" IDENT
+| WITH operconstr0 "%" scope
 | MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")"
 | MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
 ]
@@ -364,6 +374,11 @@ pattern10: [
 | DELETE pattern1
 ]
 
+pattern1: [
+| REPLACE pattern0 "%" IDENT
+| WITH pattern0 "%" scope
+]
+
 pattern0: [
 | REPLACE "(" pattern200 ")"
 | WITH "(" LIST1 pattern200 SEP "|" ")"
@@ -419,6 +434,8 @@ gallina: [
 | WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition )
 | REPLACE "Scheme" LIST1 scheme SEP "with"
 | WITH "Scheme" scheme LIST0 ( "with" scheme )
+| REPLACE "Primitive" identref OPT [ ":" lconstr ] ":=" register_token
+| WITH "Primitive" identref OPT [ ":" lconstr ] ":=" "#" identref
 ]
 
 constructor_list_or_record_decl: [
@@ -494,10 +511,6 @@ strategy_flag: [
 | OPTINREF
 ]
 
-export_token: [
-| OPTINREF
-]
-
 functor_app_annot: [
 | OPTINREF
 ]
@@ -536,20 +549,23 @@ gallina_ext: [
 | REPLACE "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 identref ]
 | WITH "Generalizable" [  [ "Variable" | "Variables" ] LIST1 identref | "All" "Variables" | "No" "Variables" ]
 
+(* don't show Export for Set, Unset *)
 | REPLACE "Export" "Set" option_table option_setting
-| WITH OPT "Export" "Set" option_table option_setting
+| WITH "Set" option_table option_setting
 | REPLACE "Export" "Unset" option_table
-| WITH OPT "Export" "Unset" option_table
+| WITH "Unset" option_table
 | REPLACE "Instance" instance_name ":" operconstr200 hint_info [ ":=" "{" record_declaration "}" | ":=" lconstr | ]
 | WITH "Instance" instance_name ":" operconstr200 hint_info OPT [ ":=" "{" record_declaration "}" | ":=" lconstr ]
 
+| REPLACE "From" global "Require" export_token LIST1 global
+| WITH "From" dirpath "Require" export_token LIST1 global
 ]
 
-(* lexer stuff *)
-IDENT: [
-| ident
+export_token: [
+| OPTINREF
 ]
 
+(* lexer stuff *)
 integer: [ | DELETENT ]
 RENAME: [
 | integer int (* todo: review uses in .mlg files, some should be "natural" *)
@@ -859,6 +875,7 @@ bar_cbrace: [
 printable: [
 | REPLACE [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string
 | WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string
+| DELETE "Term" smart_global OPT univ_name_list  (* readded in commands *)
 | INSERTALL "Print"
 ]
 
@@ -878,15 +895,18 @@ command: [
 | DELETE "Back"
 | REPLACE "Back" natural
 | WITH "Back" OPT natural
-| REPLACE "Test" option_table "for" LIST1 option_ref_value
-| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value )
-| DELETE "Test" option_table
 | REPLACE "Load" [ "Verbose" | ] [ ne_string | IDENT ]
 | WITH "Load" OPT "Verbose" [ ne_string | IDENT ]
 | DELETE "Unset" option_table
-| DELETE "Set" option_table option_setting
+| REPLACE "Set" option_table option_setting
+| WITH OPT "Export" "Set" option_table   (* set flag *)
+| REPLACE "Test" option_table "for" LIST1 option_ref_value
+| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value )
+| DELETE "Test" option_table
+
+(* hide the fact that table names are limited to 2 IDENTs *)
 | REPLACE "Add" IDENT IDENT LIST1 option_ref_value
-| WITH "Add" IDENT OPT IDENT LIST1 option_ref_value
+| WITH "Add" option_table LIST1 option_ref_value
 | DELETE "Add" IDENT LIST1 option_ref_value
 | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
 | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident
@@ -941,7 +961,11 @@ command: [
 | REPLACE "Preterm" "of" ident
 | WITH "Preterm" OPT ( "of" ident )
 | DELETE "Preterm"
-| EDIT "Remove" ADD_OPT IDENT IDENT LIST1 option_ref_value
+
+(* hide the fact that table names are limited to 2 IDENTs *)
+| REPLACE "Remove" IDENT IDENT LIST1 option_ref_value
+| WITH "Remove" option_table LIST1 option_ref_value
+| DELETE "Remove" IDENT LIST1 option_ref_value
 | DELETE "Restore" "State" IDENT
 | DELETE "Restore" "State" ne_string
 | "Restore" "State" [ IDENT | ne_string ]
@@ -976,6 +1000,16 @@ command: [
 | REPLACE "Abort" identref
 | WITH "Abort" OPT [ "All" | identref ]
 
+(* show the locate options as separate commands *)
+| DELETE "Locate" locatable
+| locatable
+| REPLACE "Print" smart_global OPT univ_name_list
+| WITH "Print" OPT "Term" smart_global OPT univ_name_list
+
+]
+
+option_setting: [
+| OPTINREF
 ]
 
 only_parsing: [
@@ -1062,9 +1096,7 @@ legacy_attr: [
 | DELETE "NonCumulative"
 ]
 
-vernacular: [
-| LIST0 ( OPT all_attrs [ command | tactic ] "." )
-]
+sentence: [ ]  (* productions defined below *)
 
 rec_definition: [
 | REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations
@@ -1124,7 +1156,7 @@ query_command: [
 | 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_query searchabout_queries
+| WITH "Search" searchabout_queries
 ]
 
 vernac_toplevel: [
@@ -1142,37 +1174,25 @@ vernac_toplevel: [
 | DELETE vernac_control
 ]
 
-positive_search_mark: [
-| OPTINREF
-]
-
 in_or_out_modules: [
 | OPTINREF
 ]
 
-searchabout_queries: [
-| OPTINREF
-]
-
 vernac_control: [
 (* replacing vernac_control with command is cheating a little;
    they can't refer to the vernac_toplevel commands.
    cover this the descriptions of these commands *)
 | REPLACE "Time" vernac_control
-| WITH "Time" command
+| WITH "Time" sentence
 | REPLACE "Redirect" ne_string vernac_control
-| WITH "Redirect" ne_string command
+| WITH "Redirect" ne_string sentence
 | REPLACE "Timeout" natural vernac_control
-| WITH "Timeout" natural command
+| WITH "Timeout" natural sentence
 | REPLACE "Fail" vernac_control
-| WITH "Fail" command
+| WITH "Fail" sentence
 | DELETE decorated_vernac
 ]
 
-option_setting: [
-| OPTINREF
-]
-
 orient: [
 | OPTINREF
 ]
@@ -1351,6 +1371,51 @@ module_expr: [
 | DELETE module_expr module_expr_atom
 ]
 
+locatable: [
+| INSERTALL "Locate"
+]
+
+ne_in_or_out_modules: [
+| REPLACE "inside" LIST1 global
+| WITH [ "inside" | "outside" ] LIST1 global
+| 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: [
+| DELETE ne_in_or_out_modules
+| REPLACE searchabout_query searchabout_queries
+| WITH LIST1 ( positive_search_mark searchabout_query ) OPT ne_in_or_out_modules
+| DELETE (* empty *)
+]
+
+positive_search_mark: [
+| OPTINREF
+]
+
+by_notation: [
+| REPLACE ne_string OPT [ "%" IDENT ]
+| WITH ne_string OPT [ "%" scope ]
+]
+
+scope_delimiter: [
+| REPLACE "%" IDENT
+| WITH "%" scope
+]
+
+(* Don't show these details *)
+DELETE: [
+| register_token
+| register_prim_token
+| register_type_token
+]
+
 SPLICE: [
 | noedit_mode
 | bigint
@@ -1435,9 +1500,7 @@ SPLICE: [
 | mode
 | mult_pattern
 | open_constr
-| option_table
 | record_declaration
-| register_type_token
 | tactic
 | uconstr
 | impl_ident_head
@@ -1466,14 +1529,12 @@ SPLICE: [
 | assum_coe
 | inline
 | occs
-| univ_name_list
 | ltac_info
 | field_mods
 | ltac_production_sep
 | ltac_tactic_level
 | printunivs_subgraph
 | ring_mods
-| scope_delimiter
 | eliminator  (* todo: splice or not? *)
 | quoted_attributes  (* todo: splice or not? *)
 | printable
@@ -1486,7 +1547,6 @@ SPLICE: [
 | option_ref_value
 | positive_search_mark
 | in_or_out_modules
-| register_prim_token
 | option_setting
 | orient
 | with_bindings
@@ -1518,6 +1578,10 @@ SPLICE: [
 | ltac_def_kind
 | intropatterns
 | instance_name
+| ne_in_or_out_modules
+| searchabout_queries
+| locatable
+| scope_delimiter
 ] (* end SPLICE *)
 
 RENAME: [
@@ -1567,8 +1631,12 @@ RENAME: [
 | record_binder_body field_body
 | class_rawexpr class
 | smart_global smart_qualid
+| searchabout_query search_item
+| option_table setting_name
 ]
 
+(* 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
@@ -1656,3 +1724,18 @@ SPLICE: [
 | tactic_notation_tactics
 ]
 (* todo: ssrreflect*.rst ref to fix_body is incorrect *)
+
+(* not included in insertprodn; defined in rst with :production: *)
+control_command: [ ]
+query_command: [ ] (* re-add since previously spliced *)
+
+sentence: [
+| OPT all_attrs command "."
+| OPT all_attrs OPT ( num ":" ) query_command "."
+| OPT all_attrs OPT toplevel_selector ltac_expr [ "." | "..." ]
+| control_command
+]
+
+vernacular: [
+| LIST0 sentence
+]
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index eea1d5081d..f00fda0e8c 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -189,6 +189,9 @@ let rec db_output_prodn = function
 and db_out_list prod = sprintf "(%s)" (map_and_concat db_output_prodn prod)
 and db_out_prods prods = sprintf "( %s )" (map_and_concat ~delim:" | " db_out_list prods)
 
+(* identify special chars that don't get a trailing space in output *)
+let omit_space s = List.mem s ["?"; "."; "#"]
+
 let rec output_prod plist need_semi = function
     | Sterm s -> if plist then sprintf "%s" s else sprintf "\"%s\"" s
     | Snterm s ->
@@ -225,7 +228,7 @@ let rec output_prod plist need_semi = function
 
 and prod_to_str_r plist prod =
   match prod with
-  | Sterm s :: Snterm "ident" :: tl when List.mem s ["?"; "."] && plist ->
+  | Sterm s :: Snterm "ident" :: tl when omit_space s && plist ->
     (sprintf "%s`ident`" s) :: (prod_to_str_r plist tl)
   | p :: tl ->
     let need_semi =
@@ -282,7 +285,7 @@ and output_sep sep =
 
 and prod_to_prodn_r prod =
   match prod with
-  | Sterm s :: Snterm "ident" :: tl when List.mem s ["?"; "."] ->
+  | Sterm s :: Snterm "ident" :: tl when omit_space s ->
     (sprintf "%s@ident" s) :: (prod_to_prodn_r tl)
   | p :: tl -> (output_prodn p) :: (prod_to_prodn_r tl)
   | [] -> []
@@ -1621,6 +1624,7 @@ let open_temp_bin file =
   open_out_bin (sprintf "%s.new" file)
 
 let match_cmd_regex = Str.regexp "[a-zA-Z0-9_ ]+"
+let match_subscripts = Str.regexp "__[a-zA-Z0-9]+"
 
 let find_longest_match prods str =
   let get_pfx str = String.trim (if Str.string_match match_cmd_regex str 0 then Str.matched_string str else "") in
@@ -1634,19 +1638,26 @@ let find_longest_match prods str =
     in
     aux 0
   in
+  let remove_subscrs str = Str.global_replace match_subscripts "" str in
 
   let slen = String.length str in
   let str_pfx = get_pfx str in
+  let no_subscrs = remove_subscrs str in
+  let has_subscrs = no_subscrs <> str in
   let rec longest best multi best_len prods =
     match prods with
     | [] -> best, multi, best_len
     | prod :: tl ->
       let pstr = String.trim prod in  (* todo: should be pretrimmed *)
       let clen = common_prefix_len str pstr in
-      if str_pfx = "" || str_pfx <> get_pfx pstr then
+      if has_subscrs && no_subscrs = pstr then
+        str, false, clen (* exact match ignoring subscripts *)
+      else if pstr = str then
+        pstr, false, clen  (* exact match of full line *)
+      else if str_pfx = "" || str_pfx <> get_pfx pstr then
         longest best multi best_len tl  (* prefixes don't match *)
       else if clen = slen && slen = String.length pstr then
-        pstr, false, clen  (* exact match *)
+        pstr, false, clen  (* exact match on prefix *)
       else if clen > best_len then
         longest pstr false clen tl  (* better match *)
       else if clen = best_len then
@@ -1654,7 +1665,11 @@ let find_longest_match prods str =
       else
         longest best multi best_len tl  (* worse match *)
   in
-  longest "" false 0 prods
+  let mtch, multi, _ = longest "" false 0 prods in
+  if has_subscrs && mtch <> str then
+    "", multi, mtch (* no match for subscripted entry *)
+  else
+    mtch, multi, ""
 
 type seen = {
   nts: (string * int) NTMap.t;
@@ -1753,8 +1768,14 @@ let process_rst g file args seen tac_prods cmd_prods =
 (*  in*)
 
   let cmd_replace_files = [
+    "doc/sphinx/language/core/records.rst";
+    "doc/sphinx/language/core/sections.rst";
+    "doc/sphinx/language/extensions/implicit-arguments.rst";
+    "doc/sphinx/language/using/libraries/funind.rst";
+
     "doc/sphinx/language/gallina-specification-language.rst";
-    "doc/sphinx/language/gallina-extensions.rst"
+    "doc/sphinx/language/gallina-extensions.rst";
+    "doc/sphinx/proof-engine/vernacular-commands.rst"
   ]
   in
 
@@ -1763,11 +1784,14 @@ let process_rst g file args seen tac_prods cmd_prods =
       if StringSet.is_empty prods || not (List.mem file cmd_replace_files) then
         rhs (* no change *)
       else
-        let mtch, multi, len = find_longest_match prods rhs in
+        let mtch, multi, best = find_longest_match prods rhs in
+(*        Printf.printf "mtch = '%s'  rhs = '%s'\n" mtch rhs;*)
         if mtch = rhs then
           rhs (* no change *)
         else if mtch = "" then begin
           warn "%s line %d: NO MATCH `%s`\n" file !linenum rhs;
+          if best <> "" then
+            warn "%s line %d: BEST `%s`\n" file !linenum best;
           rhs
         end else if multi then begin
           warn "%s line %d: MULTIMATCH `%s`\n" file !linenum rhs;
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 535976b7d9..ac986f9adf 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -47,7 +47,7 @@ one_term: [
 
 term1: [
 | term_projection
-| term0 "%" ident
+| term0 "%" scope
 | term0
 ]
 
@@ -159,7 +159,20 @@ where: [
 ]
 
 vernacular: [
-| LIST0 ( OPT all_attrs [ command | ltac_expr ] "." )
+| LIST0 sentence
+]
+
+sentence: [
+| OPT all_attrs command "."
+| OPT all_attrs OPT ( num ":" ) query_command "."
+| OPT all_attrs OPT toplevel_selector ltac_expr [ "." | "..." ]
+| control_command
+]
+
+control_command: [
+]
+
+query_command: [
 ]
 
 tacticals: [
@@ -330,7 +343,7 @@ pattern10: [
 ]
 
 pattern1: [
-| pattern0 "%" ident
+| pattern0 "%" scope
 | pattern0
 ]
 
@@ -367,53 +380,6 @@ decl_notation: [
 | string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" ident ]
 ]
 
-register_token: [
-| "#int63_type"
-| "#float64_type"
-| "#int63_head0"
-| "#int63_tail0"
-| "#int63_add"
-| "#int63_sub"
-| "#int63_mul"
-| "#int63_div"
-| "#int63_mod"
-| "#int63_lsr"
-| "#int63_lsl"
-| "#int63_land"
-| "#int63_lor"
-| "#int63_lxor"
-| "#int63_addc"
-| "#int63_subc"
-| "#int63_addcarryc"
-| "#int63_subcarryc"
-| "#int63_mulc"
-| "#int63_diveucl"
-| "#int63_div21"
-| "#int63_addmuldiv"
-| "#int63_eq"
-| "#int63_lt"
-| "#int63_le"
-| "#int63_compare"
-| "#float64_opp"
-| "#float64_abs"
-| "#float64_eq"
-| "#float64_lt"
-| "#float64_le"
-| "#float64_compare"
-| "#float64_classify"
-| "#float64_add"
-| "#float64_sub"
-| "#float64_mul"
-| "#float64_div"
-| "#float64_sqrt"
-| "#float64_of_int63"
-| "#float64_normfr_mantissa"
-| "#float64_frshiftexp"
-| "#float64_ldshiftexp"
-| "#float64_next_up"
-| "#float64_next_down"
-]
-
 thm_token: [
 | "Theorem"
 | "Lemma"
@@ -601,20 +567,20 @@ smart_qualid: [
 ]
 
 by_notation: [
-| string OPT [ "%" ident ]
+| string OPT [ "%" scope ]
 ]
 
 argument_spec_block: [
 | argument_spec
 | "/"
 | "&"
-| "(" LIST1 argument_spec ")" OPT ( "%" ident )
-| "[" LIST1 argument_spec "]" OPT ( "%" ident )
-| "{" LIST1 argument_spec "}" OPT ( "%" ident )
+| "(" LIST1 argument_spec ")" OPT ( "%" scope )
+| "[" LIST1 argument_spec "]" OPT ( "%" scope )
+| "{" LIST1 argument_spec "}" OPT ( "%" scope )
 ]
 
 argument_spec: [
-| OPT "!" name OPT ( "%" ident )
+| OPT "!" name OPT ( "%" scope )
 ]
 
 more_implicits_block: [
@@ -637,10 +603,14 @@ arguments_modifier: [
 | "extra" "scopes"
 ]
 
+scope: [
+| ident
+]
+
 strategy_level: [
-| "expand"
 | "opaque"
 | int
+| "expand"
 | "transparent"
 ]
 
@@ -660,12 +630,16 @@ command: [
 | "Cd" OPT string
 | "Load" OPT "Verbose" [ string | ident ]
 | "Declare" "ML" "Module" LIST1 string
-| "Locate" locatable
+| "Locate" smart_qualid
+| "Locate" "Term" smart_qualid
+| "Locate" "Module" qualid
+| "Locate" "Ltac" qualid
+| "Locate" "Library" qualid
+| "Locate" "File" string
 | "Add" "LoadPath" string "as" dirpath
 | "Add" "Rec" "LoadPath" string "as" dirpath
 | "Remove" "LoadPath" string
 | "Type" term
-| "Print" "Term" smart_qualid OPT ( "@{" LIST0 name "}" )
 | "Print" "All"
 | "Print" "Section" qualid
 | "Print" "Grammar" ident
@@ -702,18 +676,17 @@ command: [
 | "Print" "Strategy" smart_qualid
 | "Print" "Strategies"
 | "Print" "Registered"
-| "Print" smart_qualid OPT ( "@{" LIST0 name "}" )
+| "Print" OPT "Term" smart_qualid OPT univ_name_list
 | "Print" "Module" "Type" qualid
 | "Print" "Module" qualid
 | "Print" "Namespace" dirpath
 | "Inspect" num
 | "Add" "ML" "Path" string
-| OPT "Export" "Set" LIST1 ident OPT [ int | string ]
-| OPT "Export" "Unset" LIST1 ident
-| "Print" "Table" LIST1 ident
-| "Add" ident OPT ident LIST1 [ qualid | string ]
-| "Test" LIST1 ident OPT ( "for" LIST1 [ qualid | string ] )
-| "Remove" OPT ident ident LIST1 [ qualid | string ]
+| OPT "Export" "Set" setting_name
+| "Print" "Table" setting_name
+| "Add" setting_name LIST1 [ qualid | string ]
+| "Test" setting_name OPT ( "for" LIST1 [ qualid | string ] )
+| "Remove" setting_name LIST1 [ qualid | string ]
 | "Write" "State" [ ident | string ]
 | "Restore" "State" [ ident | string ]
 | "Reset" "Initial"
@@ -806,7 +779,6 @@ command: [
 | "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr
 | "Print" "Rewrite" "HintDb" ident
 | "Print" "Ltac" qualid
-| "Locate" "Ltac" qualid
 | "Ltac" tacdef_body LIST0 ( "with" tacdef_body )
 | "Print" "Ltac" "Signatures"
 | "Set" "Firstorder" "Solver" ltac_expr
@@ -861,7 +833,7 @@ command: [
 | "Combined" "Scheme" ident "from" LIST1 ident SEP ","
 | "Register" qualid "as" qualid
 | "Register" "Inline" qualid
-| "Primitive" ident OPT [ ":" term ] ":=" register_token
+| "Primitive" ident OPT [ ":" term ] ":=" "#" ident
 | "Universe" LIST1 ident
 | "Universes" LIST1 ident
 | "Constraint" LIST1 univ_constraint SEP ","
@@ -876,7 +848,7 @@ command: [
 | "End" ident
 | "Collection" ident ":=" section_subset_expr
 | "Require" OPT [ "Import" | "Export" ] LIST1 qualid
-| "From" qualid "Require" OPT [ "Import" | "Export" ] LIST1 qualid
+| "From" dirpath "Require" OPT [ "Import" | "Export" ] LIST1 qualid
 | "Import" LIST1 qualid
 | "Export" LIST1 qualid
 | "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
@@ -898,6 +870,8 @@ command: [
 | "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ]
 | "Implicit" [ "Type" | "Types" ] reserv_list
 | "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ]
+| "Set" setting_name OPT [ int | string ]
+| "Unset" setting_name
 | "Open" "Scope" ident
 | "Close" "Scope" ident
 | "Delimit" "Scope" ident "with" ident
@@ -912,15 +886,15 @@ command: [
 | "Eval" red_expr "in" term
 | "Compute" term
 | "Check" term
-| "About" smart_qualid OPT ( "@{" LIST0 name "}" )
-| "SearchHead" one_term OPT ne_in_or_out_modules
-| "SearchPattern" one_term OPT ne_in_or_out_modules
-| "SearchRewrite" one_term OPT ne_in_or_out_modules
-| "Search" searchabout_query OPT searchabout_queries
-| "Time" command
-| "Redirect" string command
-| "Timeout" num command
-| "Fail" command
+| "About" smart_qualid OPT univ_name_list
+| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "Search" LIST1 ( OPT "-" search_item ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "Time" sentence
+| "Redirect" string sentence
+| "Timeout" num sentence
+| "Fail" sentence
 | "Drop"
 | "Quit"
 | "BackTo" num
@@ -959,20 +933,15 @@ starredidentref: [
 ]
 
 dirpath: [
-| ident
-| dirpath field_ident
+| LIST0 ( ident "." ) ident
 ]
 
 bignat: [
 | numeral
 ]
 
-locatable: [
-| smart_qualid
-| "Term" smart_qualid
-| "File" string
-| "Library" qualid
-| "Module" qualid
+setting_name: [
+| LIST1 ident
 ]
 
 comment: [
@@ -981,6 +950,15 @@ comment: [
 | num
 ]
 
+search_item: [
+| one_term
+| string OPT ( "%" scope )
+]
+
+univ_name_list: [
+| "@{" LIST0 name "}"
+]
+
 hint: [
 | "Resolve" LIST1 [ qualid | one_term ] OPT hint_info
 | "Resolve" "->" LIST1 qualid OPT num
@@ -1068,21 +1046,6 @@ class: [
 | smart_qualid
 ]
 
-ne_in_or_out_modules: [
-| "inside" LIST1 qualid
-| "outside" LIST1 qualid
-]
-
-searchabout_query: [
-| OPT "-" string OPT ( "%" ident )
-| OPT "-" one_term
-]
-
-searchabout_queries: [
-| ne_in_or_out_modules
-| searchabout_query searchabout_queries
-]
-
 level: [
 | "level" num
 | "next" "level"