Skip to content

Commit 5b14a0b

Browse files
author
GitHub Actions
committed
Deploy mimuw-jnp2-rust/mimuw-jnp2-rust.github.io to mimuw-jnp2-rust/mimuw-jnp2-rust.github.io:gh-pages
0 parents  commit 5b14a0b

File tree

186 files changed

+36341
-0
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

186 files changed

+36341
-0
lines changed

404.html

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
<!doctype html>
2+
<title>404 Not Found</title>
3+
<h1>404 Not Found</h1>

atom.xml

Lines changed: 9224 additions & 0 deletions
Large diffs are not rendered by default.

book.css

Lines changed: 1 addition & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

book.js

Lines changed: 232 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,232 @@
1+
let elasticlunr;
2+
3+
function initToggleMenu() {
4+
const $menu = document.querySelector(".menu");
5+
const $menuIcon = document.querySelector(".menu-icon");
6+
const $page = document.querySelector(".page");
7+
$menuIcon.addEventListener("click", () => {
8+
$menu.classList.toggle("menu-hidden");
9+
$page.classList.toggle("page-without-menu");
10+
});
11+
}
12+
13+
function debounce(func, wait) {
14+
let timeout;
15+
16+
return () => {
17+
const context = this;
18+
const args = arguments;
19+
clearTimeout(timeout);
20+
21+
timeout = setTimeout(() => {
22+
timeout = null;
23+
func.apply(context, args);
24+
}, wait);
25+
};
26+
}
27+
28+
// Taken from mdbook
29+
// The strategy is as follows:
30+
// First, assign a value to each word in the document:
31+
// Words that correspond to search terms (stemmer aware): 40
32+
// Normal words: 2
33+
// First word in a sentence: 8
34+
// Then use a sliding window with a constant number of words and count the
35+
// sum of the values of the words within the window. Then use the window that got the
36+
// maximum sum. If there are multiple maximas, then get the last one.
37+
// Enclose the terms in <b>.
38+
function makeTeaser(body, terms) {
39+
const TERM_WEIGHT = 40;
40+
const NORMAL_WORD_WEIGHT = 2;
41+
const FIRST_WORD_WEIGHT = 8;
42+
const TEASER_MAX_WORDS = 30;
43+
44+
const stemmedTerms = terms.map((w) => elasticlunr.stemmer(w.toLowerCase()));
45+
let termFound = false;
46+
let index = 0;
47+
const weighted = []; // contains elements of ["word", weight, index_in_document]
48+
49+
// split in sentences, then words
50+
const sentences = body.toLowerCase().split(". ");
51+
52+
for (const i in sentences) {
53+
const words = sentences[i].split(" ");
54+
let value = FIRST_WORD_WEIGHT;
55+
56+
for (const j in words) {
57+
const word = words[j];
58+
59+
if (word.length > 0) {
60+
for (const k in stemmedTerms) {
61+
if (elasticlunr.stemmer(word).startsWith(stemmedTerms[k])) {
62+
value = TERM_WEIGHT;
63+
termFound = true;
64+
}
65+
}
66+
weighted.push([word, value, index]);
67+
value = NORMAL_WORD_WEIGHT;
68+
}
69+
70+
index += word.length;
71+
index += 1; // ' ' or '.' if last word in sentence
72+
}
73+
74+
index += 1; // because we split at a two-char boundary '. '
75+
}
76+
77+
if (weighted.length === 0) {
78+
return body;
79+
}
80+
81+
const windowWeights = [];
82+
const windowSize = Math.min(weighted.length, TEASER_MAX_WORDS);
83+
// We add a window with all the weights first
84+
let curSum = 0;
85+
for (let i = 0; i < windowSize; i++) {
86+
curSum += weighted[i][1];
87+
}
88+
windowWeights.push(curSum);
89+
90+
for (let i = 0; i < weighted.length - windowSize; i++) {
91+
curSum -= weighted[i][1];
92+
curSum += weighted[i + windowSize][1];
93+
windowWeights.push(curSum);
94+
}
95+
96+
// If we didn't find the term, just pick the first window
97+
let maxSumIndex = 0;
98+
if (termFound) {
99+
let maxFound = 0;
100+
// backwards
101+
for (let i = windowWeights.length - 1; i >= 0; i--) {
102+
if (windowWeights[i] > maxFound) {
103+
maxFound = windowWeights[i];
104+
maxSumIndex = i;
105+
}
106+
}
107+
}
108+
109+
const teaser = [];
110+
let startIndex = weighted[maxSumIndex][2];
111+
for (let i = maxSumIndex; i < maxSumIndex + windowSize; i++) {
112+
const word = weighted[i];
113+
if (startIndex < word[2]) {
114+
// missing text from index to start of `word`
115+
teaser.push(body.substring(startIndex, word[2]));
116+
startIndex = word[2];
117+
}
118+
119+
// add <em/> around search terms
120+
if (word[1] === TERM_WEIGHT) {
121+
teaser.push("<b>");
122+
}
123+
startIndex = word[2] + word[0].length;
124+
teaser.push(body.substring(word[2], startIndex));
125+
126+
if (word[1] === TERM_WEIGHT) {
127+
teaser.push("</b>");
128+
}
129+
}
130+
teaser.push("…");
131+
return teaser.join("");
132+
}
133+
134+
function formatSearchResultItem(item, terms) {
135+
const li = document.createElement("li");
136+
li.classList.add("search-results__item");
137+
li.innerHTML = `<a href="${item.ref}">${item.doc.title}</a>`;
138+
li.innerHTML += `<div class="search-results__teaser">${makeTeaser(
139+
item.doc.body,
140+
terms
141+
)}</div>`;
142+
return li;
143+
}
144+
145+
// Go from the book view to the search view
146+
function toggleSearchMode() {
147+
const $bookContent = document.querySelector(".book-content");
148+
const $searchContainer = document.querySelector(".search-container");
149+
if ($searchContainer.classList.contains("search-container--is-visible")) {
150+
$searchContainer.classList.remove("search-container--is-visible");
151+
document.body.classList.remove("search-mode");
152+
$bookContent.style.display = "block";
153+
} else {
154+
$searchContainer.classList.add("search-container--is-visible");
155+
document.body.classList.add("search-mode");
156+
$bookContent.style.display = "none";
157+
document.getElementById("search").focus();
158+
}
159+
}
160+
161+
function initSearch() {
162+
const $searchInput = document.getElementById("search");
163+
if (!$searchInput) {
164+
return;
165+
}
166+
const $searchIcon = document.querySelector(".search-icon");
167+
$searchIcon.addEventListener("click", toggleSearchMode);
168+
169+
const $searchResults = document.querySelector(".search-results");
170+
const $searchResultsHeader = document.querySelector(
171+
".search-results__header"
172+
);
173+
const $searchResultsItems = document.querySelector(".search-results__items");
174+
const MAX_ITEMS = 10;
175+
176+
const options = {
177+
bool: "AND",
178+
fields: {
179+
title: { boost: 2 },
180+
body: { boost: 1 },
181+
},
182+
};
183+
let currentTerm = "";
184+
const index = elasticlunr.Index.load(window.searchIndex);
185+
186+
$searchInput.addEventListener(
187+
"keyup",
188+
debounce(() => {
189+
const term = $searchInput.value.trim();
190+
if (term === currentTerm || !index) {
191+
return;
192+
}
193+
$searchResults.style.display = term === "" ? "none" : "block";
194+
$searchResultsItems.innerHTML = "";
195+
if (term === "") {
196+
return;
197+
}
198+
199+
const results = index
200+
.search(term, options)
201+
.filter((r) => r.doc.body !== "");
202+
if (results.length === 0) {
203+
$searchResultsHeader.innerText = `No search results for '${term}'.`;
204+
return;
205+
}
206+
207+
currentTerm = term;
208+
$searchResultsHeader.innerText = `${results.length} search results for '${term}':`;
209+
for (let i = 0; i < Math.min(results.length, MAX_ITEMS); i++) {
210+
if (!results[i].doc.body) {
211+
continue;
212+
}
213+
214+
$searchResultsItems.appendChild(
215+
formatSearchResultItem(results[i], term.split(" "))
216+
);
217+
}
218+
}, 150)
219+
);
220+
}
221+
222+
if (
223+
document.readyState === "complete" ||
224+
(document.readyState !== "loading" && !document.documentElement.doScroll)
225+
) {
226+
initToggleMenu();
227+
} else {
228+
document.addEventListener("DOMContentLoaded", () => {
229+
initToggleMenu();
230+
initSearch();
231+
});
232+
}

elasticlunr.min.js

Lines changed: 10 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)