Browse Source

build based on 517f0a6

gh-pages
Documenter.jl 2 years ago
parent
commit
4ccfc5352f
  1. 2
      v1.3.0/.documenter-siteinfo.json
  2. 508
      v1.3.0/assets/documenter.js
  3. 2
      v1.3.0/assets/themes/documenter-dark.css
  4. 2
      v1.3.0/assets/themes/documenter-light.css
  5. 12
      v1.3.0/index.html
  6. 6
      v1.3.0/objects.inv

2
v1.3.0/.documenter-siteinfo.json

@ -1 +1 @@ @@ -1 +1 @@
{"documenter":{"julia_version":"1.10.2","generation_timestamp":"2024-03-08T11:08:18","documenter_version":"1.1.2"}}
{"documenter":{"julia_version":"1.10.2","generation_timestamp":"2024-04-16T09:06:07","documenter_version":"1.4.0"}}

508
v1.3.0/assets/documenter.js

@ -4,7 +4,6 @@ requirejs.config({ @@ -4,7 +4,6 @@ requirejs.config({
'highlight-julia': 'https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.8.0/languages/julia.min',
'headroom': 'https://cdnjs.cloudflare.com/ajax/libs/headroom/0.12.0/headroom.min',
'jqueryui': 'https://cdnjs.cloudflare.com/ajax/libs/jqueryui/1.13.2/jquery-ui.min',
'minisearch': 'https://cdn.jsdelivr.net/npm/minisearch@6.1.0/dist/umd/index.min',
'katex-auto-render': 'https://cdnjs.cloudflare.com/ajax/libs/KaTeX/0.16.8/contrib/auto-render.min',
'jquery': 'https://cdnjs.cloudflare.com/ajax/libs/jquery/3.7.0/jquery.min',
'headroom-jquery': 'https://cdnjs.cloudflare.com/ajax/libs/headroom/0.12.0/jQuery.headroom.min',
@ -103,9 +102,10 @@ $(document).on("click", ".docstring header", function () { @@ -103,9 +102,10 @@ $(document).on("click", ".docstring header", function () {
});
});
$(document).on("click", ".docs-article-toggle-button", function () {
$(document).on("click", ".docs-article-toggle-button", function (event) {
let articleToggleTitle = "Expand docstring";
let navArticleToggleTitle = "Expand all docstrings";
let animationSpeed = event.noToggleAnimation ? 0 : 400;
debounce(() => {
if (isExpanded) {
@ -116,7 +116,7 @@ $(document).on("click", ".docs-article-toggle-button", function () { @@ -116,7 +116,7 @@ $(document).on("click", ".docs-article-toggle-button", function () {
isExpanded = false;
$(".docstring section").slideUp();
$(".docstring section").slideUp(animationSpeed);
} else {
$(this).removeClass("fa-chevron-down").addClass("fa-chevron-up");
$(".docstring-article-toggle-button")
@ -127,7 +127,7 @@ $(document).on("click", ".docs-article-toggle-button", function () { @@ -127,7 +127,7 @@ $(document).on("click", ".docs-article-toggle-button", function () {
articleToggleTitle = "Collapse docstring";
navArticleToggleTitle = "Collapse all docstrings";
$(".docstring section").slideDown();
$(".docstring section").slideDown(animationSpeed);
}
$(this).prop("title", navArticleToggleTitle);
@ -224,15 +224,93 @@ $(document).ready(function () { @@ -224,15 +224,93 @@ $(document).ready(function () {
})
////////////////////////////////////////////////////////////////////////////////
require(['jquery', 'minisearch'], function($, minisearch) {
require(['jquery'], function($) {
$(document).ready(function () {
let meta = $("div[data-docstringscollapsed]").data();
if (meta?.docstringscollapsed) {
$("#documenter-article-toggle-button").trigger({
type: "click",
noToggleAnimation: true,
});
}
});
})
////////////////////////////////////////////////////////////////////////////////
require(['jquery'], function($) {
/*
To get an in-depth about the thought process you can refer: https://hetarth02.hashnode.dev/series/gsoc
PSEUDOCODE:
Searching happens automatically as the user types or adjusts the selected filters.
To preserve responsiveness, as much as possible of the slow parts of the search are done
in a web worker. Searching and result generation are done in the worker, and filtering and
DOM updates are done in the main thread. The filters are in the main thread as they should
be very quick to apply. This lets filters be changed without re-searching with minisearch
(which is possible even if filtering is on the worker thread) and also lets filters be
changed _while_ the worker is searching and without message passing (neither of which are
possible if filtering is on the worker thread)
SEARCH WORKER:
Import minisearch
// In general, most search related things will have "search" as a prefix.
// To get an in-depth about the thought process you can refer: https://hetarth02.hashnode.dev/series/gsoc
Build index
let results = [];
let timer = undefined;
On message from main thread
run search
find the first 200 unique results from each category, and compute their divs for display
note that this is necessary and sufficient information for the main thread to find the
first 200 unique results from any given filter set
post results to main thread
let data = documenterSearchIndex["docs"].map((x, key) => {
MAIN:
Launch worker
Declare nonconstant globals (worker_is_running, last_search_text, unfiltered_results)
On text update
if worker is not running, launch_search()
launch_search
set worker_is_running to true, set last_search_text to the search text
post the search query to worker
on message from worker
if last_search_text is not the same as the text in the search field,
the latest search result is not reflective of the latest search query, so update again
launch_search()
otherwise
set worker_is_running to false
regardless, display the new search results to the user
save the unfiltered_results as a global
update_search()
on filter click
adjust the filter selection
update_search()
update_search
apply search filters by looping through the unfiltered_results and finding the first 200
unique results that match the filters
Update the DOM
*/
/////// SEARCH WORKER ///////
function worker_function(documenterSearchIndex, documenterBaseURL, filters) {
importScripts(
"https://cdn.jsdelivr.net/npm/minisearch@6.1.0/dist/umd/index.min.js"
);
let data = documenterSearchIndex.map((x, key) => {
x["id"] = key; // minisearch requires a unique for each object
return x;
});
@ -348,9 +426,9 @@ const stopWords = new Set([ @@ -348,9 +426,9 @@ const stopWords = new Set([
"your",
]);
let index = new minisearch({
let index = new MiniSearch({
fields: ["title", "text"], // fields to index for full-text search
storeFields: ["location", "title", "text", "category", "page"], // fields to return with search results
storeFields: ["location", "title", "text", "category", "page"], // fields to return with results
processTerm: (term) => {
let word = stopWords.has(term) ? null : term;
if (word) {
@ -358,180 +436,58 @@ let index = new minisearch({ @@ -358,180 +436,58 @@ let index = new minisearch({
word = word
.replace(/^[^a-zA-Z0-9@!]+/, "")
.replace(/[^a-zA-Z0-9@!]+$/, "");
word = word.toLowerCase();
}
return word ?? null;
},
// add . as a separator, because otherwise "title": "Documenter.Anchors.add!", would not find anything if searching for "add!", only for the entire qualification
// add . as a separator, because otherwise "title": "Documenter.Anchors.add!", would not
// find anything if searching for "add!", only for the entire qualification
tokenize: (string) => string.split(/[\s\-\.]+/),
// options which will be applied during the search
searchOptions: {
prefix: true,
boost: { title: 100 },
fuzzy: 2,
processTerm: (term) => {
let word = stopWords.has(term) ? null : term;
if (word) {
word = word
.replace(/^[^a-zA-Z0-9@!]+/, "")
.replace(/[^a-zA-Z0-9@!]+$/, "");
}
return word ?? null;
},
tokenize: (string) => string.split(/[\s\-\.]+/),
},
});
index.addAll(data);
let filters = [...new Set(data.map((x) => x.category))];
var modal_filters = make_modal_body_filters(filters);
var filter_results = [];
$(document).on("keyup", ".documenter-search-input", function (event) {
// Adding a debounce to prevent disruptions from super-speed typing!
debounce(() => update_search(filter_results), 300);
});
$(document).on("click", ".search-filter", function () {
if ($(this).hasClass("search-filter-selected")) {
$(this).removeClass("search-filter-selected");
} else {
$(this).addClass("search-filter-selected");
}
// Adding a debounce to prevent disruptions from crazy clicking!
debounce(() => get_filters(), 300);
});
/**
* A debounce function, takes a function and an optional timeout in milliseconds
*
* @function callback
* @param {number} timeout
* Used to map characters to HTML entities.
* Refer: https://github.com/lodash/lodash/blob/main/src/escape.ts
*/
function debounce(callback, timeout = 300) {
clearTimeout(timer);
timer = setTimeout(callback, timeout);
}
const htmlEscapes = {
"&": "&",
"<": "&lt;",
">": "&gt;",
'"': "&quot;",
"'": "&#39;",
};
/**
* Make/Update the search component
*
* @param {string[]} selected_filters
* Used to match HTML entities and HTML characters.
* Refer: https://github.com/lodash/lodash/blob/main/src/escape.ts
*/
function update_search(selected_filters = []) {
let initial_search_body = `
<div class="has-text-centered my-5 py-5">Type something to get started!</div>
`;
let querystring = $(".documenter-search-input").val();
if (querystring.trim()) {
results = index.search(querystring, {
filter: (result) => {
// Filtering results
if (selected_filters.length === 0) {
return result.score >= 1;
} else {
return (
result.score >= 1 && selected_filters.includes(result.category)
);
}
},
});
let search_result_container = ``;
let search_divider = `<div class="search-divider w-100"></div>`;
if (results.length) {
let links = [];
let count = 0;
let search_results = "";
results.forEach(function (result) {
if (result.location) {
// Checking for duplication of results for the same page
if (!links.includes(result.location)) {
search_results += make_search_result(result, querystring);
count++;
}
links.push(result.location);
}
});
let result_count = `<div class="is-size-6">${count} result(s)</div>`;
search_result_container = `
<div class="is-flex is-flex-direction-column gap-2 is-align-items-flex-start">
${modal_filters}
${search_divider}
${result_count}
<div class="is-clipped w-100 is-flex is-flex-direction-column gap-2 is-align-items-flex-start has-text-justified mt-1">
${search_results}
</div>
</div>
`;
} else {
search_result_container = `
<div class="is-flex is-flex-direction-column gap-2 is-align-items-flex-start">
${modal_filters}
${search_divider}
<div class="is-size-6">0 result(s)</div>
</div>
<div class="has-text-centered my-5 py-5">No result found!</div>
`;
}
if ($(".search-modal-card-body").hasClass("is-justify-content-center")) {
$(".search-modal-card-body").removeClass("is-justify-content-center");
}
$(".search-modal-card-body").html(search_result_container);
} else {
filter_results = [];
modal_filters = make_modal_body_filters(filters, filter_results);
if (!$(".search-modal-card-body").hasClass("is-justify-content-center")) {
$(".search-modal-card-body").addClass("is-justify-content-center");
}
$(".search-modal-card-body").html(initial_search_body);
}
}
const reUnescapedHtml = /[&<>"']/g;
const reHasUnescapedHtml = RegExp(reUnescapedHtml.source);
/**
* Make the modal filter html
*
* @param {string[]} filters
* @param {string[]} selected_filters
* @returns string
* Escape function from lodash
* Refer: https://github.com/lodash/lodash/blob/main/src/escape.ts
*/
function make_modal_body_filters(filters, selected_filters = []) {
let str = ``;
filters.forEach((val) => {
if (selected_filters.includes(val)) {
str += `<a href="javascript:;" class="search-filter search-filter-selected"><span>${val}</span></a>`;
} else {
str += `<a href="javascript:;" class="search-filter"><span>${val}</span></a>`;
}
});
let filter_html = `
<div class="is-flex gap-2 is-flex-wrap-wrap is-justify-content-flex-start is-align-items-center search-filters">
<span class="is-size-6">Filters:</span>
${str}
</div>
`;
return filter_html;
function escape(string) {
return string && reHasUnescapedHtml.test(string)
? string.replace(reUnescapedHtml, (chr) => htmlEscapes[chr])
: string || "";
}
/**
* Make the result component given a minisearch result data object and the value of the search input as queryString.
* To view the result object structure, refer: https://lucaong.github.io/minisearch/modules/_minisearch_.html#searchresult
* Make the result component given a minisearch result data object and the value
* of the search input as queryString. To view the result object structure, refer:
* https://lucaong.github.io/minisearch/modules/_minisearch_.html#searchresult
*
* @param {object} result
* @param {string} querystring
@ -547,7 +503,7 @@ function make_search_result(result, querystring) { @@ -547,7 +503,7 @@ function make_search_result(result, querystring) {
display_link += ` (${result.page})`;
}
let textindex = new RegExp(`\\b${querystring}\\b`, "i").exec(result.text);
let textindex = new RegExp(`${querystring}`, "i").exec(result.text);
let text =
textindex !== null
? result.text.slice(
@ -559,11 +515,13 @@ function make_search_result(result, querystring) { @@ -559,11 +515,13 @@ function make_search_result(result, querystring) {
)
: ""; // cut-off text before and after from the match
text = text.length ? escape(text) : "";
let display_result = text.length
? "..." +
text.replace(
new RegExp(`\\b${querystring}\\b`, "i"), // For first occurrence
'<span class="search-result-highlight p-1">$&</span>'
new RegExp(`${escape(querystring)}`, "i"), // For first occurrence
'<span class="search-result-highlight py-1">$&</span>'
) +
"..."
: ""; // highlights the match
@ -581,7 +539,7 @@ function make_search_result(result, querystring) { @@ -581,7 +539,7 @@ function make_search_result(result, querystring) {
<div class="w-100 is-flex is-flex-wrap-wrap is-justify-content-space-between is-align-items-flex-start">
<div class="search-result-title has-text-weight-bold ${
in_code ? "search-result-code-title" : ""
}">${result.title}</div>
}">${escape(result.title)}</div>
<div class="property-search-result-badge">${result.category}</div>
</div>
<p>
@ -601,14 +559,213 @@ function make_search_result(result, querystring) { @@ -601,14 +559,213 @@ function make_search_result(result, querystring) {
return result_div;
}
self.onmessage = function (e) {
let query = e.data;
let results = index.search(query, {
filter: (result) => {
// Only return relevant results
return result.score >= 1;
},
});
// Pre-filter to deduplicate and limit to 200 per category to the extent
// possible without knowing what the filters are.
let filtered_results = [];
let counts = {};
for (let filter of filters) {
counts[filter] = 0;
}
let present = {};
for (let result of results) {
cat = result.category;
cnt = counts[cat];
if (cnt < 200) {
id = cat + "---" + result.location;
if (present[id]) {
continue;
}
present[id] = true;
filtered_results.push({
location: result.location,
category: cat,
div: make_search_result(result, query),
});
}
}
postMessage(filtered_results);
};
}
// `worker = Threads.@spawn worker_function(documenterSearchIndex)`, but in JavaScript!
const filters = [
...new Set(documenterSearchIndex["docs"].map((x) => x.category)),
];
const worker_str =
"(" +
worker_function.toString() +
")(" +
JSON.stringify(documenterSearchIndex["docs"]) +
"," +
JSON.stringify(documenterBaseURL) +
"," +
JSON.stringify(filters) +
")";
const worker_blob = new Blob([worker_str], { type: "text/javascript" });
const worker = new Worker(URL.createObjectURL(worker_blob));
/////// SEARCH MAIN ///////
// Whether the worker is currently handling a search. This is a boolean
// as the worker only ever handles 1 or 0 searches at a time.
var worker_is_running = false;
// The last search text that was sent to the worker. This is used to determine
// if the worker should be launched again when it reports back results.
var last_search_text = "";
// The results of the last search. This, in combination with the state of the filters
// in the DOM, is used compute the results to display on calls to update_search.
var unfiltered_results = [];
// Which filter is currently selected
var selected_filter = "";
$(document).on("input", ".documenter-search-input", function (event) {
if (!worker_is_running) {
launch_search();
}
});
function launch_search() {
worker_is_running = true;
last_search_text = $(".documenter-search-input").val();
worker.postMessage(last_search_text);
}
worker.onmessage = function (e) {
if (last_search_text !== $(".documenter-search-input").val()) {
launch_search();
} else {
worker_is_running = false;
}
unfiltered_results = e.data;
update_search();
};
$(document).on("click", ".search-filter", function () {
if ($(this).hasClass("search-filter-selected")) {
selected_filter = "";
} else {
selected_filter = $(this).text().toLowerCase();
}
// This updates search results and toggles classes for UI:
update_search();
});
/**
* Make/Update the search component
*/
function update_search() {
let querystring = $(".documenter-search-input").val();
if (querystring.trim()) {
if (selected_filter == "") {
results = unfiltered_results;
} else {
results = unfiltered_results.filter((result) => {
return selected_filter == result.category.toLowerCase();
});
}
let search_result_container = ``;
let modal_filters = make_modal_body_filters();
let search_divider = `<div class="search-divider w-100"></div>`;
if (results.length) {
let links = [];
let count = 0;
let search_results = "";
for (var i = 0, n = results.length; i < n && count < 200; ++i) {
let result = results[i];
if (result.location && !links.includes(result.location)) {
search_results += result.div;
count++;
links.push(result.location);
}
}
if (count == 1) {
count_str = "1 result";
} else if (count == 200) {
count_str = "200+ results";
} else {
count_str = count + " results";
}
let result_count = `<div class="is-size-6">${count_str}</div>`;
search_result_container = `
<div class="is-flex is-flex-direction-column gap-2 is-align-items-flex-start">
${modal_filters}
${search_divider}
${result_count}
<div class="is-clipped w-100 is-flex is-flex-direction-column gap-2 is-align-items-flex-start has-text-justified mt-1">
${search_results}
</div>
</div>
`;
} else {
search_result_container = `
<div class="is-flex is-flex-direction-column gap-2 is-align-items-flex-start">
${modal_filters}
${search_divider}
<div class="is-size-6">0 result(s)</div>
</div>
<div class="has-text-centered my-5 py-5">No result found!</div>
`;
}
if ($(".search-modal-card-body").hasClass("is-justify-content-center")) {
$(".search-modal-card-body").removeClass("is-justify-content-center");
}
$(".search-modal-card-body").html(search_result_container);
} else {
if (!$(".search-modal-card-body").hasClass("is-justify-content-center")) {
$(".search-modal-card-body").addClass("is-justify-content-center");
}
$(".search-modal-card-body").html(`
<div class="has-text-centered my-5 py-5">Type something to get started!</div>
`);
}
}
/**
* Get selected filters, remake the filter html and lastly update the search modal
* Make the modal filter html
*
* @returns string
*/
function get_filters() {
let ele = $(".search-filters .search-filter-selected").get();
filter_results = ele.map((x) => $(x).text().toLowerCase());
modal_filters = make_modal_body_filters(filters, filter_results);
update_search(filter_results);
function make_modal_body_filters() {
let str = filters
.map((val) => {
if (selected_filter == val.toLowerCase()) {
return `<a href="javascript:;" class="search-filter search-filter-selected"><span>${val}</span></a>`;
} else {
return `<a href="javascript:;" class="search-filter"><span>${val}</span></a>`;
}
})
.join("");
return `
<div class="is-flex gap-2 is-flex-wrap-wrap is-justify-content-flex-start is-align-items-center search-filters">
<span class="is-size-6">Filters:</span>
${str}
</div>`;
}
})
@ -635,6 +792,7 @@ $(document).ready(function () { @@ -635,6 +792,7 @@ $(document).ready(function () {
////////////////////////////////////////////////////////////////////////////////
require(['jquery'], function($) {
$(document).ready(function () {
let search_modal_header = `
<header class="modal-card-head gap-2 is-align-items-center is-justify-content-space-between w-100 px-3">
<div class="field mb-0 w-100">
@ -680,8 +838,13 @@ $(document.body).append( @@ -680,8 +838,13 @@ $(document.body).append(
`
);
document.querySelector(".docs-search-query").addEventListener("click", () => {
openModal();
});
document.querySelector(".close-search-modal").addEventListener("click", () => {
document
.querySelector(".close-search-modal")
.addEventListener("click", () => {
closeModal();
});
@ -729,6 +892,7 @@ document @@ -729,6 +892,7 @@ document
.addEventListener("click", () => {
closeModal();
});
});
})
////////////////////////////////////////////////////////////////////////////////

2
v1.3.0/assets/themes/documenter-dark.css

File diff suppressed because one or more lines are too long

2
v1.3.0/assets/themes/documenter-light.css

File diff suppressed because one or more lines are too long

12
v1.3.0/index.html

File diff suppressed because one or more lines are too long

6
v1.3.0/objects.inv

@ -0,0 +1,6 @@ @@ -0,0 +1,6 @@
# Sphinx inventory version 2
# Project: Prometheus.jl
# Version: 1.3.0
# The remainder of this file is compressed using zlib.
xœ¥V]o›0}ϯ°´ñ¦,<EFBFBD>T©ÚÃ2ºv•¦¨k»çŠš›”pdÌÖ*ÊßóacâœsϹ\'Î"x%¹ˆ."F‰ÿ‘<EFBFBD>[ÎRÏPä^’Ùu°$*÷W·7>‡ pÈ(Tœ$|‚¤d½{O$A$i‘³o¯;–Ç"f™AògA‘ –ú´áæF"H‡˜]‡ÅÆì”˜žL<EFBFBD>Bžw>M;7™à,*¨Ã­ŒjžkE³eÉŠL€Mð{ŒÙmy˜ŽäÓâz9Ýiò7Käú—‘¸ _<EFBFBD>ª6ÓŒ| ›°HFÝ¢+‹x  ËÒ]›ŸM<EFBFBD>{lüÙÏ"¦¿sraùñNZ‹ÁÆìʈ7c®t“?J¨Mæ*Lãd¬AdNr3oPÿ¡Ø%°W«9<EFBFBD>“;yI.Ês hczç_û\oxËEÉ÷Î/õgO9ð?`жMÖ"èâmŒòõ—ò÷ØÂl;'òÓ-©pPP¢¥DýÜù"âªp!å¬Íû´¨~Ö4<EFBFBD><EFBFBD>›U‘ýs;Shz)$Ñ4g;Ž%Â<EFBFBD>°§€ôÚ)û\Z¨Y‹þ ;9ˆGÁiÁq2ñËâ<EFBFBD>3†m0û ¼]ªNmŠLîms)£Â‰/IË<î%éÖúqsÚãM›Uc]IÍ«ºn5;Eª!g§n›–y\!›[ì¸2j¬iEt®µ:Ö,µ:Â@–Íx\–kZ–ÕÍ’û¿2lî^ª­s"Ÿ‚öÉXCû`NJà*{;Èßg¼‡ˆ<sºS¥Ð\cr<EFBFBD>ž¤Åæ$0N,[Q¤££•ò¹üº¨ á§ŽÓSç<EFBFBD><EFBFBD>=u3áÏ(`&½væ«ÆÌ×–<EFBFBD>wxg«2¥ Y®-W•—ÿäýåÈ•ÕÂ\&ñ'ì„z6OÜ
5{à<EFBFBD>©ÿ;©ÝìÆW<EFBFBD>ôN/jH¥<EFBFBD>æxZÞ3g¯´ýT’è
Loading…
Cancel
Save