blob: 4562219f6e21aed00cce03e133c01540d2bfd224 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
<link rel="prefetch" href="{{root}}search-index.json" />
<link rel="prefetch" href="{{root}}search-metadata.json" />
<div id="search_placeholder">
<p>Search is loading. If you cannot see any results after a few seconds, check that JavaScript is enabled in your browser.</p>
</div>
<div id="search_noquery">
<p>Enter a few words to the box above to start the search.</p>
</div>
<div id="search_success" style="display: none">
<h1>Search results</h1>
<div id="search_results">
</div>
</div>
<div id="search_fail" style="display: none">
<h1>No results found</h1>
<p>You may try a simpler search query, or find the page <a href="{{root}}tag">by the categories</a>.</p>
</div>
<div id="search_error" style="display: none">
<h1>Search error</h1>
<p>Search failed; this is likely caused by a badly formatted query string. Try a different query.</p>
<p>The error description is: <span style="color: red" id="search_error_text"></span></p>
</div>
<script src="{{root}}static/lunr.min.js"></script>
<script>
var el_query = document.getElementById('search_query');
var el_placeholder = document.getElementById('search_placeholder');
var el_noquery = document.getElementById('search_noquery');
var el_success = document.getElementById('search_success');
var el_fail = document.getElementById('search_fail');
var el_error = document.getElementById('search_error');
var el_error_text = document.getElementById('search_error_text');
var el_results = document.getElementById('search_results');
function run_search(q) {
el_placeholder.style.display = 'none';
if(q.length === 0) {
el_noquery.style.display = 'block';
el_success.style.display = 'none';
el_fail.style.display = 'none';
el_error.style.display = 'none';
return;
}
var results = []
try {
results = window.search_index.search(q)
} catch (err) {
console.log("search error: " + err);
el_error_text.innerHTML = '';
el_error_text.appendChild(document.createTextNode(err.message));
el_noquery.style.display = 'none';
el_success.style.display = 'none';
el_fail.style.display = 'none';
el_error.style.display = 'block';
return;
}
el_results.innerHTML = ''
for(var ri=0; ri<results.length; ++ri) {
if (ri>=100) {
var out = document.createElement("p")
out.innerHTML = "Displaying only 100 top matches. Try searching for more specific terms to refine the search."
el_results.appendChild(out)
break;
}
const r=results[ri]
var out = document.createElement("p")
out.appendChild(document.createTextNode(window.search_metadata[r.ref].title))
el_results.appendChild(out)
}
if(results.length === 0) {
el_noquery.style.display = 'none';
el_success.style.display = 'none';
el_fail.style.display = 'block';
el_error.style.display = 'none';
} else {
el_noquery.style.display = 'none';
el_success.style.display = 'block';
el_fail.style.display = 'none';
el_error.style.display = 'none';
}
}
function handle_search_input(ev) {
run_search(ev.target.value)
window.history.pushState("", "", window.location.pathname + '?search_query='+encodeURIComponent(ev.target.value))
el_query.addEventListener('input', handle_search_input)
}
Promise.all([
fetch('{{root}}search-index.json').then(response => response.text()).then(text => {
window.search_index = lunr.Index.load(JSON.parse(text))
}),
fetch('{{root}}search-metadata.json').then(response => response.text()).then(text => {
window.search_metadata = JSON.parse(text)
})
]).then(() => {
var search_term = (new URLSearchParams(window.location.search)).get('search_query') || "";
el_query.value = search_term
handle_search_input({target: {value: search_term}})
})
</script>
|
