diff options
| author | Jim Fehrle | 2020-04-10 14:42:37 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-04-10 15:00:57 -0700 |
| commit | 90cffaab81a733fc49f6a985f0d7b44900e70d59 (patch) | |
| tree | e70f21b92043024c8d8f08e09b525e097e27d31a | |
| parent | c5c8ce135606f311834d4c0b9ac3e72be5ee4a36 (diff) | |
Fix prefix matching
| -rw-r--r-- | doc/tools/docgram/doc_grammar.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index eea1d5081d..8d3bcdd866 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -1643,10 +1643,12 @@ let find_longest_match prods str = | 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 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 |