Skip to content

Commit 05ced24

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 05ced24

File tree

188 files changed

+34333
-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.

188 files changed

+34333
-0
lines changed

.nojekyll

Whitespace-only changes.

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

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)