You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We compute the string index of each query word which matches the result's name in query/name_cost.ml, but then only keep the total of the costs. If we also preserved the indexes, we could explain the results by highlighting the matching parts of the names with <mark>.
Doing the same for the documentation comments will require do a similar search but on html (which isn't done yet, as we just assume a query word not found in the name will be in the comment!). It'll be even harder to have a similar highlight for types, since their pretty-pretting is handled by odoc so we don't know which substrings to highlight... We can probably do follow-up PRs for those, name matching would already be a great first step.
The text was updated successfully, but these errors were encountered:
We compute the string index of each query word which matches the result's name in query/name_cost.ml, but then only keep the total of the costs. If we also preserved the indexes, we could explain the results by highlighting the matching parts of the names with
<mark>
.Doing the same for the documentation comments will require do a similar search but on html (which isn't done yet, as we just assume a query word not found in the name will be in the comment!). It'll be even harder to have a similar highlight for types, since their pretty-pretting is handled by odoc so we don't know which substrings to highlight... We can probably do follow-up PRs for those, name matching would already be a great first step.
The text was updated successfully, but these errors were encountered: