| 46 | |
| 47 | |
| 48 | async function initialize() { |
| 49 | /* Get the search index and compile it if necessary. |
| 50 | This function will only be called once. */ |
| 51 | try { |
| 52 | search = await new Promise((resolve, reject) => { |
| 53 | const script = document.createElement("script"); |
| 54 | script.type = "text/javascript"; |
| 55 | script.async = true; |
| 56 | script.onload = () => resolve(window.docsSearch); |
| 57 | script.onerror = (e) => reject(e); |
| 58 | script.src = root + "/searchindex.js"; |
| 59 | document.getElementsByTagName("head")[0].appendChild(script); |
| 60 | }); |
| 61 | } catch (e) { |
| 62 | searchErr = "Cannot fetch search index."; |
| 63 | } |
| 64 | onInput(); |
| 65 | } |
| 66 | |
| 67 | function onInput() { |
| 68 | setContent((() => { |