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 turn the JSON index into a JavaScript file. In order to never block the UI, this file will be used as a web worker by [odoc] to perform searches:
808
808
809
809
- The search query will be sent as a plain string to the web worker, using the standard mechanism of message passing.
810
-
- The web worker has to send back the result as a message to the main thread, containing the list of result. Each entry of this list must have the same form it had in the original JSON file.
810
+
- The web worker has to send back the result as a message to the main thread, containing the list of results. Each entry of this list must have the same form it had in the original JSON file.
811
811
- The file must be given to the [odoc-support] URI.
812
812
813
813
In this driver, we use the MiniSearch JavaScript library. For more involved applications, we could use [index.js] to call a server-side search engine via an API call.
0 commit comments