RFC: search for keywords in any order

[tom93]

Hi, will you accept a PR to change the behaviour of the Search feature to include results that contain the search patterns in any order?

Currently, if I search for Vector toArray toList on https://leanprover-community.github.io/mathlib4_docs/, I don't get any results. I would like to see Vector.toList_toArray in the results.

There was some old code that did order-independent matching (over the entire docstring), but it was removed in commit 08de0ad. At the moment spaces are removed from the search pattern and have no effect at all.

I propose augmenting the current (fuzzy) search results with declarations that contain exact matches for the words in the search pattern in any order.

For ranking the results, I suggest the following:

1. Results that contain exact matches for the words in the same order as the pattern (within this group, sort by the fuzzy match error).
2. Results that contain exact matches in a different order (again sorted by fuzzy match error).
3. All other results (sorted by fuzzy match error).

[hargoniX]

One of the main things to consider with the fuzzy matching in doc-gen is that you are searching through a database of several 100k strings in a browser. A lot of the perceived stupidity of the fuzzy search by the users is intended because on lower end machines it would just freeze the browser if there was a fancy algorithm. If you can write an implementation that doesn't have a relevant performance regression I would be happy to accept it but otherwise I'd rather keep the page usable for everyone.