Ignore subscripts in notation for matching cmds and tacs

1 files changed, 16 insertions, 3 deletions

diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 8d3bcdd866..77273cdc5b 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -1621,6 +1621,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,16 +1635,21 @@ 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 pstr = str 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 *)
@@ -1656,7 +1662,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;
@@ -1765,11 +1775,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;