pub static JS: &'static [u8] = b"\"use strict\";\nwindow.search = window.search || {};\n(function search(search) {\n // Search functionality\n //\n // You can use !hasFocus() to prevent keyhandling in your key\n // event handlers while the user is typing their search.\n\n if (!Mark || !elasticlunr) {\n return;\n }\n\n //IE 11 Compatibility from https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/String/startsWith\n if (!String.prototype.startsWith) {\n String.prototype.startsWith = function(search, pos) {\n return this.substr(!pos || pos < 0 ? 0 : +pos, search.length) === search;\n };\n }\n\n var search_wrap = document.getElementById(\'search-wrapper\'),\n searchbar = document.getElementById(\'searchbar\'),\n searchbar_outer = document.getElementById(\'searchbar-outer\'),\n searchresults = document.getElementById(\'searchresults\'),\n searchresults_outer = document.getElementById(\'searchresults-outer\'),\n searchresults_header = document.getElementById(\'searchresults-header\'),\n searchicon = document.getElementById(\'search-toggle\'),\n content = document.getElementById(\'content\'),\n\n searchindex = null,\n doc_urls = [],\n results_options = {\n teaser_word_count: 30,\n limit_results: 30,\n },\n search_options = {\n bool: \"AND\",\n expand: true,\n fields: {\n title: {boost: 1},\n body: {boost: 1},\n breadcrumbs: {boost: 0}\n }\n },\n mark_exclude = [],\n marker = new Mark(content),\n current_searchterm = \"\",\n URL_SEARCH_PARAM = \'search\',\n URL_MARK_PARAM = \'highlight\',\n teaser_count = 0,\n\n SEARCH_HOTKEY_KEYCODE = 83,\n ESCAPE_KEYCODE = 27,\n DOWN_KEYCODE = 40,\n UP_KEYCODE = 38,\n SELECT_KEYCODE = 13;\n\n function hasFocus() {\n return searchbar === document.activeElement;\n }\n\n function removeChildren(elem) {\n while (elem.firstChild) {\n elem.removeChild(elem.firstChild);\n }\n }\n\n // Helper to parse a url into its building blocks.\n function parseURL(url) {\n var a = document.createElement(\'a\');\n a.href = url;\n return {\n source: url,\n protocol: a.protocol.replace(\':\',\'\'),\n host: a.hostname,\n port: a.port,\n params: (function(){\n var ret = {};\n var seg = a.search.replace(/^\\?/,\'\').split(\'&\');\n var len = seg.length, i = 0, s;\n for (;i<len;i++) {\n if (!seg[i]) { continue; }\n s = seg[i].split(\'=\');\n ret[s[0]] = s[1];\n }\n return ret;\n })(),\n file: (a.pathname.match(/\\/([^/?#]+)$/i) || [,\'\'])[1],\n hash: a.hash.replace(\'#\',\'\'),\n path: a.pathname.replace(/^([^/])/,\'/$1\')\n };\n }\n \n // Helper to recreate a url string from its building blocks.\n function renderURL(urlobject) {\n var url = urlobject.protocol + \"://\" + urlobject.host;\n if (urlobject.port != \"\") {\n url += \":\" + urlobject.port;\n }\n url += urlobject.path;\n var joiner = \"?\";\n for(var prop in urlobject.params) {\n if(urlobject.params.hasOwnProperty(prop)) {\n url += joiner + prop + \"=\" + urlobject.params[prop];\n joiner = \"&\";\n }\n }\n if (urlobject.hash != \"\") {\n url += \"#\" + urlobject.hash;\n }\n return url;\n }\n \n // Helper to escape html special chars for displaying the teasers\n var escapeHTML = (function() {\n var MAP = {\n \'&\': \'&\',\n \'<\': \'<\',\n \'>\': \'>\',\n \'\"\': \'"\',\n \"\'\": \''\'\n };\n var repl = function(c) { return MAP[c]; };\n return function(s) {\n return s.replace(/[&<>\'\"]/g, repl);\n };\n })();\n \n function formatSearchMetric(count, searchterm) {\n if (count == 1) {\n return count + \" search result for \'\" + searchterm + \"\':\";\n } else if (count == 0) {\n return \"No search results for \'\" + searchterm + \"\'.\";\n } else {\n return count + \" search results for \'\" + searchterm + \"\':\";\n }\n }\n \n function formatSearchResult(result, searchterms) {\n var teaser = makeTeaser(escapeHTML(result.doc.body), searchterms);\n teaser_count++;\n\n // The ?URL_MARK_PARAM= parameter belongs inbetween the page and the #heading-anchor\n var url = doc_urls[result.ref].split(\"#\");\n if (url.length == 1) { // no anchor found\n url.push(\"\");\n }\n\n return \'<a href=\"\' + path_to_root + url[0] + \'?\' + URL_MARK_PARAM + \'=\' + searchterms + \'#\' + url[1]\n + \'\" aria-details=\"teaser_\' + teaser_count + \'\">\' + result.doc.breadcrumbs + \'</a>\'\n + \'<span class=\"teaser\" id=\"teaser_\' + teaser_count + \'\" aria-label=\"Search Result Teaser\">\' \n + teaser + \'</span>\';\n }\n \n function makeTeaser(body, searchterms) {\n // The strategy is as follows:\n // First, assign a value to each word in the document:\n // Words that correspond to search terms (stemmer aware): 40\n // Normal words: 2\n // First word in a sentence: 8\n // Then use a sliding window with a constant number of words and count the\n // sum of the values of the words within the window. Then use the window that got the\n // maximum sum. If there are multiple maximas, then get the last one.\n // Enclose the terms in <em>.\n var stemmed_searchterms = searchterms.map(function(w) {\n return elasticlunr.stemmer(w.toLowerCase());\n });\n var searchterm_weight = 40;\n var weighted = []; // contains elements of [\"word\", weight, index_in_document]\n // split in sentences, then words\n var sentences = body.toLowerCase().split(\'. \');\n var index = 0;\n var value = 0;\n var searchterm_found = false;\n for (var sentenceindex in sentences) {\n var words = sentences[sentenceindex].split(\' \');\n value = 8;\n for (var wordindex in words) {\n var word = words[wordindex];\n if (word.length > 0) {\n for (var searchtermindex in stemmed_searchterms) {\n if (elasticlunr.stemmer(word).startsWith(stemmed_searchterms[searchtermindex])) {\n value = searchterm_weight;\n searchterm_found = true;\n }\n };\n weighted.push([word, value, index]);\n value = 2;\n }\n index += word.length;\n index += 1; // \' \' or \'.\' if last word in sentence\n };\n index += 1; // because we split at a two-char boundary \'. \'\n };\n\n if (weighted.length == 0) {\n return body;\n }\n\n var window_weight = [];\n var window_size = Math.min(weighted.length, results_options.teaser_word_count);\n\n var cur_sum = 0;\n for (var wordindex = 0; wordindex < window_size; wordindex++) {\n cur_sum += weighted[wordindex][1];\n };\n window_weight.push(cur_sum);\n for (var wordindex = 0; wordindex < weighted.length - window_size; wordindex++) {\n cur_sum -= weighted[wordindex][1];\n cur_sum += weighted[wordindex + window_size][1];\n window_weight.push(cur_sum);\n };\n\n if (searchterm_found) {\n var max_sum = 0;\n var max_sum_window_index = 0;\n // backwards\n for (var i = window_weight.length - 1; i >= 0; i--) {\n if (window_weight[i] > max_sum) {\n max_sum = window_weight[i];\n max_sum_window_index = i;\n }\n };\n } else {\n max_sum_window_index = 0;\n }\n\n // add <em/> around searchterms\n var teaser_split = [];\n var index = weighted[max_sum_window_index][2];\n for (var i = max_sum_window_index; i < max_sum_window_index+window_size; i++) {\n var word = weighted[i];\n if (index < word[2]) {\n // missing text from index to start of `word`\n teaser_split.push(body.substring(index, word[2]));\n index = word[2];\n }\n if (word[1] == searchterm_weight) {\n teaser_split.push(\"<em>\")\n }\n index = word[2] + word[0].length;\n teaser_split.push(body.substring(word[2], index));\n if (word[1] == searchterm_weight) {\n teaser_split.push(\"</em>\")\n }\n };\n\n return teaser_split.join(\'\');\n }\n\n function init(config) {\n results_options = config.results_options;\n search_options = config.search_options;\n searchbar_outer = config.searchbar_outer;\n doc_urls = config.doc_urls;\n searchindex = elasticlunr.Index.load(config.index);\n\n // Set up events\n searchicon.addEventListener(\'click\', function(e) { searchIconClickHandler(); }, false);\n searchbar.addEventListener(\'keyup\', function(e) { searchbarKeyUpHandler(); }, false);\n document.addEventListener(\'keydown\', function(e) { globalKeyHandler(e); }, false);\n // If the user uses the browser buttons, do the same as if a reload happened\n window.onpopstate = function(e) { doSearchOrMarkFromUrl(); };\n // Suppress \"submit\" events so the page doesn\'t reload when the user presses Enter\n document.addEventListener(\'submit\', function(e) { e.preventDefault(); }, false);\n\n // If reloaded, do the search or mark again, depending on the current url parameters\n doSearchOrMarkFromUrl();\n }\n \n function unfocusSearchbar() {\n // hacky, but just focusing a div only works once\n var tmp = document.createElement(\'input\');\n tmp.setAttribute(\'style\', \'position: absolute; opacity: 0;\');\n searchicon.appendChild(tmp);\n tmp.focus();\n tmp.remove();\n }\n \n // On reload or browser history backwards/forwards events, parse the url and do search or mark\n function doSearchOrMarkFromUrl() {\n // Check current URL for search request\n var url = parseURL(window.location.href);\n if (url.params.hasOwnProperty(URL_SEARCH_PARAM)\n && url.params[URL_SEARCH_PARAM] != \"\") {\n showSearch(true);\n searchbar.value = decodeURIComponent(\n (url.params[URL_SEARCH_PARAM]+\'\').replace(/\\+/g, \'%20\'));\n searchbarKeyUpHandler(); // -> doSearch()\n } else {\n showSearch(false);\n }\n\n if (url.params.hasOwnProperty(URL_MARK_PARAM)) {\n var words = url.params[URL_MARK_PARAM].split(\' \');\n marker.mark(words, {\n exclude: mark_exclude\n });\n\n var markers = document.querySelectorAll(\"mark\");\n function hide() {\n for (var i = 0; i < markers.length; i++) {\n markers[i].classList.add(\"fade-out\");\n window.setTimeout(function(e) { marker.unmark(); }, 300);\n }\n }\n for (var i = 0; i < markers.length; i++) {\n markers[i].addEventListener(\'click\', hide);\n }\n }\n }\n \n // Eventhandler for keyevents on `document`\n function globalKeyHandler(e) {\n if (e.altKey || e.ctrlKey || e.metaKey || e.shiftKey || e.target.type === \'textarea\') { return; }\n\n if (e.keyCode === ESCAPE_KEYCODE) {\n e.preventDefault();\n searchbar.classList.remove(\"active\");\n setSearchUrlParameters(\"\",\n (searchbar.value.trim() !== \"\") ? \"push\" : \"replace\");\n if (hasFocus()) {\n unfocusSearchbar();\n }\n showSearch(false);\n marker.unmark();\n } else if (!hasFocus() && e.keyCode === SEARCH_HOTKEY_KEYCODE) {\n e.preventDefault();\n showSearch(true);\n window.scrollTo(0, 0);\n searchbar.select();\n } else if (hasFocus() && e.keyCode === DOWN_KEYCODE) {\n e.preventDefault();\n unfocusSearchbar();\n searchresults.firstElementChild.classList.add(\"focus\");\n } else if (!hasFocus() && (e.keyCode === DOWN_KEYCODE\n || e.keyCode === UP_KEYCODE\n || e.keyCode === SELECT_KEYCODE)) {\n // not `:focus` because browser does annoying scrolling\n var focused = searchresults.querySelector(\"li.focus\");\n if (!focused) return;\n e.preventDefault();\n if (e.keyCode === DOWN_KEYCODE) {\n var next = focused.nextElementSibling;\n if (next) {\n focused.classList.remove(\"focus\");\n next.classList.add(\"focus\");\n }\n } else if (e.keyCode === UP_KEYCODE) {\n focused.classList.remove(\"focus\");\n var prev = focused.previousElementSibling;\n if (prev) {\n prev.classList.add(\"focus\");\n } else {\n searchbar.select();\n }\n } else { // SELECT_KEYCODE\n window.location.assign(focused.querySelector(\'a\'));\n }\n }\n }\n \n function showSearch(yes) {\n if (yes) {\n search_wrap.classList.remove(\'hidden\');\n searchicon.setAttribute(\'aria-expanded\', \'true\');\n } else {\n search_wrap.classList.add(\'hidden\');\n searchicon.setAttribute(\'aria-expanded\', \'false\');\n var results = searchresults.children;\n for (var i = 0; i < results.length; i++) {\n results[i].classList.remove(\"focus\");\n }\n }\n }\n\n function showResults(yes) {\n if (yes) {\n searchresults_outer.classList.remove(\'hidden\');\n } else {\n searchresults_outer.classList.add(\'hidden\');\n }\n }\n\n // Eventhandler for search icon\n function searchIconClickHandler() {\n if (search_wrap.classList.contains(\'hidden\')) {\n showSearch(true);\n window.scrollTo(0, 0);\n searchbar.select();\n } else {\n showSearch(false);\n }\n }\n \n // Eventhandler for keyevents while the searchbar is focused\n function searchbarKeyUpHandler() {\n var searchterm = searchbar.value.trim();\n if (searchterm != \"\") {\n searchbar.classList.add(\"active\");\n doSearch(searchterm);\n } else {\n searchbar.classList.remove(\"active\");\n showResults(false);\n removeChildren(searchresults);\n }\n\n setSearchUrlParameters(searchterm, \"push_if_new_search_else_replace\");\n\n // Remove marks\n marker.unmark();\n }\n \n // Update current url with ?URL_SEARCH_PARAM= parameter, remove ?URL_MARK_PARAM and #heading-anchor .\n // `action` can be one of \"push\", \"replace\", \"push_if_new_search_else_replace\"\n // and replaces or pushes a new browser history item.\n // \"push_if_new_search_else_replace\" pushes if there is no `?URL_SEARCH_PARAM=abc` yet.\n function setSearchUrlParameters(searchterm, action) {\n var url = parseURL(window.location.href);\n var first_search = ! url.params.hasOwnProperty(URL_SEARCH_PARAM);\n if (searchterm != \"\" || action == \"push_if_new_search_else_replace\") {\n url.params[URL_SEARCH_PARAM] = searchterm;\n delete url.params[URL_MARK_PARAM];\n url.hash = \"\";\n } else {\n delete url.params[URL_SEARCH_PARAM];\n }\n // A new search will also add a new history item, so the user can go back\n // to the page prior to searching. A updated search term will only replace\n // the url.\n if (action == \"push\" || (action == \"push_if_new_search_else_replace\" && first_search) ) {\n history.pushState({}, document.title, renderURL(url));\n } else if (action == \"replace\" || (action == \"push_if_new_search_else_replace\" && !first_search) ) {\n history.replaceState({}, document.title, renderURL(url));\n }\n }\n \n function doSearch(searchterm) {\n\n // Don\'t search the same twice\n if (current_searchterm == searchterm) { return; }\n else { current_searchterm = searchterm; }\n\n if (searchindex == null) { return; }\n\n // Do the actual search\n var results = searchindex.search(searchterm, search_options);\n var resultcount = Math.min(results.length, results_options.limit_results);\n\n // Display search metrics\n searchresults_header.innerText = formatSearchMetric(resultcount, searchterm);\n\n // Clear and insert results\n var searchterms = searchterm.split(\' \');\n removeChildren(searchresults);\n for(var i = 0; i < resultcount ; i++){\n var resultElem = document.createElement(\'li\');\n resultElem.innerHTML = formatSearchResult(results[i], searchterms);\n searchresults.appendChild(resultElem);\n }\n\n // Display results\n showResults(true);\n }\n\n fetch(path_to_root + \'searchindex.json\')\n .then(response => response.json())\n .then(json => init(json)) \n .catch(error => { // Try to load searchindex.js if fetch failed\n var script = document.createElement(\'script\');\n script.src = path_to_root + \'searchindex.js\';\n script.onload = () => init(window.search);\n document.head.appendChild(script);\n });\n\n // Exported functions\n search.hasFocus = hasFocus;\n})(window.search);\n"