+
+ Read the Docs
+ v: ${config.versions.current.slug}
+
+
+
+
+ ${renderLanguages(config)}
+ ${renderVersions(config)}
+ ${renderDownloads(config)}
+
+ - On Read the Docs
+ -
+ Project Home
+
+ -
+ Builds
+
+ -
+ Downloads
+
+
+
+ - Search
+ -
+
+
+
+
+
+ Hosted by Read the Docs
+
+
+
+ `;
+
+ // Inject the generated flyout into the body HTML element.
+ document.body.insertAdjacentHTML("beforeend", flyout);
+
+ // Trigger the Read the Docs Addons Search modal when clicking on the "Search docs" input from inside the flyout.
+ document
+ .querySelector("#flyout-search-form")
+ .addEventListener("focusin", () => {
+ const event = new CustomEvent("readthedocs-search-show");
+ document.dispatchEvent(event);
+ });
+ })
+}
+
+if (themeLanguageSelector || themeVersionSelector) {
+ function onSelectorSwitch(event) {
+ const option = event.target.selectedIndex;
+ const item = event.target.options[option];
+ window.location.href = item.dataset.url;
+ }
+
+ document.addEventListener("readthedocs-addons-data-ready", function (event) {
+ const config = event.detail.data();
+
+ const versionSwitch = document.querySelector(
+ "div.switch-menus > div.version-switch",
+ );
+ if (themeVersionSelector) {
+ let versions = config.versions.active;
+ if (config.versions.current.hidden || config.versions.current.type === "external") {
+ versions.unshift(config.versions.current);
+ }
+ const versionSelect = `
+
+ `;
+
+ versionSwitch.innerHTML = versionSelect;
+ versionSwitch.firstElementChild.addEventListener("change", onSelectorSwitch);
+ }
+
+ const languageSwitch = document.querySelector(
+ "div.switch-menus > div.language-switch",
+ );
+
+ if (themeLanguageSelector) {
+ if (config.projects.translations.length) {
+ // Add the current language to the options on the selector
+ let languages = config.projects.translations.concat(
+ config.projects.current,
+ );
+ languages = languages.sort((a, b) =>
+ a.language.name.localeCompare(b.language.name),
+ );
+
+ const languageSelect = `
+
+ `;
+
+ languageSwitch.innerHTML = languageSelect;
+ languageSwitch.firstElementChild.addEventListener("change", onSelectorSwitch);
+ }
+ else {
+ languageSwitch.remove();
+ }
+ }
+ });
+}
+
+document.addEventListener("readthedocs-addons-data-ready", function (event) {
+ // Trigger the Read the Docs Addons Search modal when clicking on "Search docs" input from the topnav.
+ document
+ .querySelector("[role='search'] input")
+ .addEventListener("focusin", () => {
+ const event = new CustomEvent("readthedocs-search-show");
+ document.dispatchEvent(event);
+ });
+});
\ No newline at end of file
diff --git a/docs/_build/html/C/_static/language_data.js b/docs/_build/html/C/_static/language_data.js
index 250f5665..c7fe6c6f 100644
--- a/docs/_build/html/C/_static/language_data.js
+++ b/docs/_build/html/C/_static/language_data.js
@@ -1,19 +1,12 @@
/*
- * language_data.js
- * ~~~~~~~~~~~~~~~~
- *
* This script contains the language-specific data used by searchtools.js,
* namely the list of stopwords, stemmer, scorer and splitter.
- *
- * :copyright: Copyright 2007-2023 by the Sphinx team, see AUTHORS.
- * :license: BSD, see LICENSE for details.
- *
*/
var stopwords = ["a", "and", "are", "as", "at", "be", "but", "by", "for", "if", "in", "into", "is", "it", "near", "no", "not", "of", "on", "or", "such", "that", "the", "their", "then", "there", "these", "they", "this", "to", "was", "will", "with"];
-/* Non-minified version is copied as a separate JS file, is available */
+/* Non-minified version is copied as a separate JS file, if available */
/**
* Porter Stemmer
diff --git a/docs/_build/html/C/_static/searchtools.js b/docs/_build/html/C/_static/searchtools.js
index 97d56a74..2c774d17 100644
--- a/docs/_build/html/C/_static/searchtools.js
+++ b/docs/_build/html/C/_static/searchtools.js
@@ -1,12 +1,5 @@
/*
- * searchtools.js
- * ~~~~~~~~~~~~~~~~
- *
* Sphinx JavaScript utilities for the full-text search.
- *
- * :copyright: Copyright 2007-2023 by the Sphinx team, see AUTHORS.
- * :license: BSD, see LICENSE for details.
- *
*/
"use strict";
@@ -20,7 +13,7 @@ if (typeof Scorer === "undefined") {
// and returns the new score.
/*
score: result => {
- const [docname, title, anchor, descr, score, filename] = result
+ const [docname, title, anchor, descr, score, filename, kind] = result
return score
},
*/
@@ -47,6 +40,14 @@ if (typeof Scorer === "undefined") {
};
}
+// Global search result kind enum, used by themes to style search results.
+class SearchResultKind {
+ static get index() { return "index"; }
+ static get object() { return "object"; }
+ static get text() { return "text"; }
+ static get title() { return "title"; }
+}
+
const _removeChildren = (element) => {
while (element && element.lastChild) element.removeChild(element.lastChild);
};
@@ -57,16 +58,20 @@ const _removeChildren = (element) => {
const _escapeRegExp = (string) =>
string.replace(/[.*+\-?^${}()|[\]\\]/g, "\\$&"); // $& means the whole matched string
-const _displayItem = (item, searchTerms) => {
+const _displayItem = (item, searchTerms, highlightTerms) => {
const docBuilder = DOCUMENTATION_OPTIONS.BUILDER;
- const docUrlRoot = DOCUMENTATION_OPTIONS.URL_ROOT;
const docFileSuffix = DOCUMENTATION_OPTIONS.FILE_SUFFIX;
const docLinkSuffix = DOCUMENTATION_OPTIONS.LINK_SUFFIX;
const showSearchSummary = DOCUMENTATION_OPTIONS.SHOW_SEARCH_SUMMARY;
+ const contentRoot = document.documentElement.dataset.content_root;
- const [docName, title, anchor, descr, score, _filename] = item;
+ const [docName, title, anchor, descr, score, _filename, kind] = item;
let listItem = document.createElement("li");
+ // Add a class representing the item's type:
+ // can be used by a theme's CSS selector for styling
+ // See SearchResultKind for the class names.
+ listItem.classList.add(`kind-${kind}`);
let requestUrl;
let linkUrl;
if (docBuilder === "dirhtml") {
@@ -75,28 +80,35 @@ const _displayItem = (item, searchTerms) => {
if (dirname.match(/\/index\/$/))
dirname = dirname.substring(0, dirname.length - 6);
else if (dirname === "index/") dirname = "";
- requestUrl = docUrlRoot + dirname;
+ requestUrl = contentRoot + dirname;
linkUrl = requestUrl;
} else {
// normal html builders
- requestUrl = docUrlRoot + docName + docFileSuffix;
+ requestUrl = contentRoot + docName + docFileSuffix;
linkUrl = docName + docLinkSuffix;
}
let linkEl = listItem.appendChild(document.createElement("a"));
linkEl.href = linkUrl + anchor;
linkEl.dataset.score = score;
linkEl.innerHTML = title;
- if (descr)
+ if (descr) {
listItem.appendChild(document.createElement("span")).innerHTML =
" (" + descr + ")";
+ // highlight search terms in the description
+ if (SPHINX_HIGHLIGHT_ENABLED) // set in sphinx_highlight.js
+ highlightTerms.forEach((term) => _highlightText(listItem, term, "highlighted"));
+ }
else if (showSearchSummary)
fetch(requestUrl)
.then((responseData) => responseData.text())
.then((data) => {
if (data)
listItem.appendChild(
- Search.makeSearchSummary(data, searchTerms)
+ Search.makeSearchSummary(data, searchTerms, anchor)
);
+ // highlight search terms in the summary
+ if (SPHINX_HIGHLIGHT_ENABLED) // set in sphinx_highlight.js
+ highlightTerms.forEach((term) => _highlightText(listItem, term, "highlighted"));
});
Search.output.appendChild(listItem);
};
@@ -108,27 +120,46 @@ const _finishSearch = (resultCount) => {
"Your search did not match any documents. Please make sure that all words are spelled correctly and that you've selected enough categories."
);
else
- Search.status.innerText = _(
- `Search finished, found ${resultCount} page(s) matching the search query.`
- );
+ Search.status.innerText = Documentation.ngettext(
+ "Search finished, found one page matching the search query.",
+ "Search finished, found ${resultCount} pages matching the search query.",
+ resultCount,
+ ).replace('${resultCount}', resultCount);
};
const _displayNextItem = (
results,
resultCount,
- searchTerms
+ searchTerms,
+ highlightTerms,
) => {
// results left, load the summary and display it
// this is intended to be dynamic (don't sub resultsCount)
if (results.length) {
- _displayItem(results.pop(), searchTerms);
+ _displayItem(results.pop(), searchTerms, highlightTerms);
setTimeout(
- () => _displayNextItem(results, resultCount, searchTerms),
+ () => _displayNextItem(results, resultCount, searchTerms, highlightTerms),
5
);
}
// search finished, update title and status message
else _finishSearch(resultCount);
};
+// Helper function used by query() to order search results.
+// Each input is an array of [docname, title, anchor, descr, score, filename, kind].
+// Order the results by score (in opposite order of appearance, since the
+// `_displayNextItem` function uses pop() to retrieve items) and then alphabetically.
+const _orderResultsByScoreThenName = (a, b) => {
+ const leftScore = a[4];
+ const rightScore = b[4];
+ if (leftScore === rightScore) {
+ // same score: sort alphabetically
+ const leftTitle = a[1].toLowerCase();
+ const rightTitle = b[1].toLowerCase();
+ if (leftTitle === rightTitle) return 0;
+ return leftTitle > rightTitle ? -1 : 1; // inverted is intentional
+ }
+ return leftScore > rightScore ? 1 : -1;
+};
/**
* Default splitQuery function. Can be overridden in ``sphinx.search`` with a
@@ -152,13 +183,26 @@ const Search = {
_queued_query: null,
_pulse_status: -1,
- htmlToText: (htmlString) => {
+ htmlToText: (htmlString, anchor) => {
const htmlElement = new DOMParser().parseFromString(htmlString, 'text/html');
- htmlElement.querySelectorAll(".headerlink").forEach((el) => { el.remove() });
+ for (const removalQuery of [".headerlink", "script", "style"]) {
+ htmlElement.querySelectorAll(removalQuery).forEach((el) => { el.remove() });
+ }
+ if (anchor) {
+ const anchorContent = htmlElement.querySelector(`[role="main"] ${anchor}`);
+ if (anchorContent) return anchorContent.textContent;
+
+ console.warn(
+ `Anchored content block not found. Sphinx search tries to obtain it via DOM query '[role=main] ${anchor}'. Check your theme or template.`
+ );
+ }
+
+ // if anchor not specified or not found, fall back to main content
const docContent = htmlElement.querySelector('[role="main"]');
- if (docContent !== undefined) return docContent.textContent;
+ if (docContent) return docContent.textContent;
+
console.warn(
- "Content block not found. Sphinx search tries to obtain it via '[role=main]'. Could you check your theme or template."
+ "Content block not found. Sphinx search tries to obtain it via DOM query '[role=main]'. Check your theme or template."
);
return "";
},
@@ -211,6 +255,7 @@ const Search = {
searchSummary.classList.add("search-summary");
searchSummary.innerText = "";
const searchList = document.createElement("ul");
+ searchList.setAttribute("role", "list");
searchList.classList.add("search");
const out = document.getElementById("search-results");
@@ -231,16 +276,7 @@ const Search = {
else Search.deferQuery(query);
},
- /**
- * execute search (requires search index to be loaded)
- */
- query: (query) => {
- const filenames = Search._index.filenames;
- const docNames = Search._index.docnames;
- const titles = Search._index.titles;
- const allTitles = Search._index.alltitles;
- const indexEntries = Search._index.indexentries;
-
+ _parseQuery: (query) => {
// stem the search terms and add them to the correct list
const stemmer = new Stemmer();
const searchTerms = new Set();
@@ -276,22 +312,40 @@ const Search = {
// console.info("required: ", [...searchTerms]);
// console.info("excluded: ", [...excludedTerms]);
- // array of [docname, title, anchor, descr, score, filename]
- let results = [];
+ return [query, searchTerms, excludedTerms, highlightTerms, objectTerms];
+ },
+
+ /**
+ * execute search (requires search index to be loaded)
+ */
+ _performSearch: (query, searchTerms, excludedTerms, highlightTerms, objectTerms) => {
+ const filenames = Search._index.filenames;
+ const docNames = Search._index.docnames;
+ const titles = Search._index.titles;
+ const allTitles = Search._index.alltitles;
+ const indexEntries = Search._index.indexentries;
+
+ // Collect multiple result groups to be sorted separately and then ordered.
+ // Each is an array of [docname, title, anchor, descr, score, filename, kind].
+ const normalResults = [];
+ const nonMainIndexResults = [];
+
_removeChildren(document.getElementById("search-progress"));
- const queryLower = query.toLowerCase();
+ const queryLower = query.toLowerCase().trim();
for (const [title, foundTitles] of Object.entries(allTitles)) {
- if (title.toLowerCase().includes(queryLower) && (queryLower.length >= title.length/2)) {
+ if (title.toLowerCase().trim().includes(queryLower) && (queryLower.length >= title.length/2)) {
for (const [file, id] of foundTitles) {
- let score = Math.round(100 * queryLower.length / title.length)
- results.push([
+ const score = Math.round(Scorer.title * queryLower.length / title.length);
+ const boost = titles[file] === title ? 1 : 0; // add a boost for document titles
+ normalResults.push([
docNames[file],
titles[file] !== title ? `${titles[file]} > ${title}` : title,
id !== null ? "#" + id : "",
null,
- score,
+ score + boost,
filenames[file],
+ SearchResultKind.title,
]);
}
}
@@ -300,46 +354,48 @@ const Search = {
// search for explicit entries in index directives
for (const [entry, foundEntries] of Object.entries(indexEntries)) {
if (entry.includes(queryLower) && (queryLower.length >= entry.length/2)) {
- for (const [file, id] of foundEntries) {
- let score = Math.round(100 * queryLower.length / entry.length)
- results.push([
+ for (const [file, id, isMain] of foundEntries) {
+ const score = Math.round(100 * queryLower.length / entry.length);
+ const result = [
docNames[file],
titles[file],
id ? "#" + id : "",
null,
score,
filenames[file],
- ]);
+ SearchResultKind.index,
+ ];
+ if (isMain) {
+ normalResults.push(result);
+ } else {
+ nonMainIndexResults.push(result);
+ }
}
}
}
// lookup as object
objectTerms.forEach((term) =>
- results.push(...Search.performObjectSearch(term, objectTerms))
+ normalResults.push(...Search.performObjectSearch(term, objectTerms))
);
// lookup as search terms in fulltext
- results.push(...Search.performTermsSearch(searchTerms, excludedTerms));
+ normalResults.push(...Search.performTermsSearch(searchTerms, excludedTerms));
// let the scorer override scores with a custom scoring function
- if (Scorer.score) results.forEach((item) => (item[4] = Scorer.score(item)));
-
- // now sort the results by score (in opposite order of appearance, since the
- // display function below uses pop() to retrieve items) and then
- // alphabetically
- results.sort((a, b) => {
- const leftScore = a[4];
- const rightScore = b[4];
- if (leftScore === rightScore) {
- // same score: sort alphabetically
- const leftTitle = a[1].toLowerCase();
- const rightTitle = b[1].toLowerCase();
- if (leftTitle === rightTitle) return 0;
- return leftTitle > rightTitle ? -1 : 1; // inverted is intentional
- }
- return leftScore > rightScore ? 1 : -1;
- });
+ if (Scorer.score) {
+ normalResults.forEach((item) => (item[4] = Scorer.score(item)));
+ nonMainIndexResults.forEach((item) => (item[4] = Scorer.score(item)));
+ }
+
+ // Sort each group of results by score and then alphabetically by name.
+ normalResults.sort(_orderResultsByScoreThenName);
+ nonMainIndexResults.sort(_orderResultsByScoreThenName);
+
+ // Combine the result groups in (reverse) order.
+ // Non-main index entries are typically arbitrary cross-references,
+ // so display them after other results.
+ let results = [...nonMainIndexResults, ...normalResults];
// remove duplicate search results
// note the reversing of results, so that in the case of duplicates, the highest-scoring entry is kept
@@ -353,14 +409,19 @@ const Search = {
return acc;
}, []);
- results = results.reverse();
+ return results.reverse();
+ },
+
+ query: (query) => {
+ const [searchQuery, searchTerms, excludedTerms, highlightTerms, objectTerms] = Search._parseQuery(query);
+ const results = Search._performSearch(searchQuery, searchTerms, excludedTerms, highlightTerms, objectTerms);
// for debugging
//Search.lastresults = results.slice(); // a copy
// console.info("search results:", Search.lastresults);
// print the results
- _displayNextItem(results, results.length, searchTerms);
+ _displayNextItem(results, results.length, searchTerms, highlightTerms);
},
/**
@@ -424,6 +485,7 @@ const Search = {
descr,
score,
filenames[match[0]],
+ SearchResultKind.object,
]);
};
Object.keys(objects).forEach((prefix) =>
@@ -458,14 +520,18 @@ const Search = {
// add support for partial matches
if (word.length > 2) {
const escapedWord = _escapeRegExp(word);
- Object.keys(terms).forEach((term) => {
- if (term.match(escapedWord) && !terms[word])
- arr.push({ files: terms[term], score: Scorer.partialTerm });
- });
- Object.keys(titleTerms).forEach((term) => {
- if (term.match(escapedWord) && !titleTerms[word])
- arr.push({ files: titleTerms[word], score: Scorer.partialTitle });
- });
+ if (!terms.hasOwnProperty(word)) {
+ Object.keys(terms).forEach((term) => {
+ if (term.match(escapedWord))
+ arr.push({ files: terms[term], score: Scorer.partialTerm });
+ });
+ }
+ if (!titleTerms.hasOwnProperty(word)) {
+ Object.keys(titleTerms).forEach((term) => {
+ if (term.match(escapedWord))
+ arr.push({ files: titleTerms[term], score: Scorer.partialTitle });
+ });
+ }
}
// no match but word was a required one
@@ -488,9 +554,8 @@ const Search = {
// create the mapping
files.forEach((file) => {
- if (fileMap.has(file) && fileMap.get(file).indexOf(word) === -1)
- fileMap.get(file).push(word);
- else fileMap.set(file, [word]);
+ if (!fileMap.has(file)) fileMap.set(file, [word]);
+ else if (fileMap.get(file).indexOf(word) === -1) fileMap.get(file).push(word);
});
});
@@ -531,6 +596,7 @@ const Search = {
null,
score,
filenames[file],
+ SearchResultKind.text,
]);
}
return results;
@@ -541,8 +607,8 @@ const Search = {
* search summary for a given text. keywords is a list
* of stemmed words.
*/
- makeSearchSummary: (htmlText, keywords) => {
- const text = Search.htmlToText(htmlText);
+ makeSearchSummary: (htmlText, keywords, anchor) => {
+ const text = Search.htmlToText(htmlText, anchor);
if (text === "") return null;
const textLower = text.toLowerCase();
diff --git a/docs/_build/html/C/_static/sphinx_highlight.js b/docs/_build/html/C/_static/sphinx_highlight.js
index aae669d7..8a96c69a 100644
--- a/docs/_build/html/C/_static/sphinx_highlight.js
+++ b/docs/_build/html/C/_static/sphinx_highlight.js
@@ -29,14 +29,19 @@ const _highlight = (node, addItems, text, className) => {
}
span.appendChild(document.createTextNode(val.substr(pos, text.length)));
+ const rest = document.createTextNode(val.substr(pos + text.length));
parent.insertBefore(
span,
parent.insertBefore(
- document.createTextNode(val.substr(pos + text.length)),
+ rest,
node.nextSibling
)
);
node.nodeValue = val.substr(0, pos);
+ /* There may be more occurrences of search term in this node. So call this
+ * function recursively on the remaining fragment.
+ */
+ _highlight(rest, addItems, text, className);
if (isInSVG) {
const rect = document.createElementNS(
@@ -140,5 +145,10 @@ const SphinxHighlight = {
},
};
-_ready(SphinxHighlight.highlightSearchWords);
-_ready(SphinxHighlight.initEscapeListener);
+_ready(() => {
+ /* Do not call highlightSearchWords() when we are on the search page.
+ * It will highlight words from the *previous* search query.
+ */
+ if (typeof Search === "undefined") SphinxHighlight.highlightSearchWords();
+ SphinxHighlight.initEscapeListener();
+});
diff --git a/docs/_build/html/C/coord_format.html b/docs/_build/html/C/coord_format.html
index 34c95142..e6580fc5 100644
--- a/docs/_build/html/C/coord_format.html
+++ b/docs/_build/html/C/coord_format.html
@@ -1,24 +1,24 @@
+
+
-
+
-
+
-
Coordinate (Coord) Format — spral v2024-05-08 [C] documentation
-
-
-
-
-
+
Coordinate (Coord) Format — spral v2025-01-08 [C] documentation
+
+
+
+
-
-
-
-
-
-
+
+
+
+
+
+
+
@@ -38,9 +38,6 @@
spral
-
- v2024-05-08 [C]
-