minisearch webworker is terminated on page reloads

[eric-wieser]

I've found the startup time for the search to be very painful, especially since when I click a search result and find its the wrong one, I have to start all over again waiting for it to load.

What's happening here is that the SharedWorker is being killed by chrome, because at the point I click the link there are no mathlib_docs tabs open with a search connection to keep it alive.

As a workaround, I can just open an extra tab and start a search in it, which is enough to keep the search alive. Better solutions might be to:

• Intercept internal page navigation and use the javascript history API to replace the page content without actually unloading the page
• Make it so I can open the search results in a new tab. (#97)

[eric-wieser]

One option for improving this would be to :

• use miniSearch.toJSON() to export the complete index after constructing it for the first time
• put it in localStorage
• next tmie a page is loaded, try using MiniSearch.fromJS(the_json_from_local_storage), which would bypass the long startup times

We'd need to make sure there's some mechanism to invalidate that cache when the docs site updates.