Skip to content

Commit

Permalink
Deploying to gh-pages from @ cf4d228 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
gares committed Feb 2, 2024
1 parent a6932a5 commit 6c8d70e
Show file tree
Hide file tree
Showing 178 changed files with 7,480 additions and 6,080 deletions.
1,188 changes: 580 additions & 608 deletions _sources/playground.rst.txt

Large diffs are not rendered by default.

123 changes: 123 additions & 0 deletions _static/_sphinx_javascript_frameworks_compat.js
Original file line number Diff line number Diff line change
@@ -0,0 +1,123 @@
/* Compatability shim for jQuery and underscores.js.
*
* Copyright Sphinx contributors
* Released under the two clause BSD licence
*/

/**
* small helper function to urldecode strings
*
* See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/decodeURIComponent#Decoding_query_parameters_from_a_URL
*/
jQuery.urldecode = function(x) {
if (!x) {
return x
}
return decodeURIComponent(x.replace(/\+/g, ' '));
};

/**
* small helper function to urlencode strings
*/
jQuery.urlencode = encodeURIComponent;

/**
* This function returns the parsed url parameters of the
* current request. Multiple values per key are supported,
* it will always return arrays of strings for the value parts.
*/
jQuery.getQueryParameters = function(s) {
if (typeof s === 'undefined')
s = document.location.search;
var parts = s.substr(s.indexOf('?') + 1).split('&');
var result = {};
for (var i = 0; i < parts.length; i++) {
var tmp = parts[i].split('=', 2);
var key = jQuery.urldecode(tmp[0]);
var value = jQuery.urldecode(tmp[1]);
if (key in result)
result[key].push(value);
else
result[key] = [value];
}
return result;
};

/**
* highlight a given string on a jquery object by wrapping it in
* span elements with the given class name.
*/
jQuery.fn.highlightText = function(text, className) {
function highlight(node, addItems) {
if (node.nodeType === 3) {
var val = node.nodeValue;
var pos = val.toLowerCase().indexOf(text);
if (pos >= 0 &&
!jQuery(node.parentNode).hasClass(className) &&
!jQuery(node.parentNode).hasClass("nohighlight")) {
var span;
var isInSVG = jQuery(node).closest("body, svg, foreignObject").is("svg");
if (isInSVG) {
span = document.createElementNS("http://www.w3.org/2000/svg", "tspan");
} else {
span = document.createElement("span");
span.className = className;
}
span.appendChild(document.createTextNode(val.substr(pos, text.length)));
node.parentNode.insertBefore(span, node.parentNode.insertBefore(
document.createTextNode(val.substr(pos + text.length)),
node.nextSibling));
node.nodeValue = val.substr(0, pos);
if (isInSVG) {
var rect = document.createElementNS("http://www.w3.org/2000/svg", "rect");
var bbox = node.parentElement.getBBox();
rect.x.baseVal.value = bbox.x;
rect.y.baseVal.value = bbox.y;
rect.width.baseVal.value = bbox.width;
rect.height.baseVal.value = bbox.height;
rect.setAttribute('class', className);
addItems.push({
"parent": node.parentNode,
"target": rect});
}
}
}
else if (!jQuery(node).is("button, select, textarea")) {
jQuery.each(node.childNodes, function() {
highlight(this, addItems);
});
}
}
var addItems = [];
var result = this.each(function() {
highlight(this, addItems);
});
for (var i = 0; i < addItems.length; ++i) {
jQuery(addItems[i].parent).before(addItems[i].target);
}
return result;
};

/*
* backward compatibility for jQuery.browser
* This will be supported until firefox bug is fixed.
*/
if (!jQuery.browser) {
jQuery.uaMatch = function(ua) {
ua = ua.toLowerCase();

var match = /(chrome)[ \/]([\w.]+)/.exec(ua) ||
/(webkit)[ \/]([\w.]+)/.exec(ua) ||
/(opera)(?:.*version|)[ \/]([\w.]+)/.exec(ua) ||
/(msie) ([\w.]+)/.exec(ua) ||
ua.indexOf("compatible") < 0 && /(mozilla)(?:.*? rv:([\w.]+)|)/.exec(ua) ||
[];

return {
browser: match[ 1 ] || "",
version: match[ 2 ] || "0"
};
};
jQuery.browser = {};
jQuery.browser[jQuery.uaMatch(navigator.userAgent).browser] = true;
}
22 changes: 22 additions & 0 deletions _static/basic.css
Original file line number Diff line number Diff line change
Expand Up @@ -237,6 +237,10 @@ a.headerlink {
visibility: hidden;
}

a:visited {
color: #551A8B;
}

h1:hover > a.headerlink,
h2:hover > a.headerlink,
h3:hover > a.headerlink,
Expand Down Expand Up @@ -670,6 +674,16 @@ dd {
margin-left: 30px;
}

.sig dd {
margin-top: 0px;
margin-bottom: 0px;
}

.sig dl {
margin-top: 0px;
margin-bottom: 0px;
}

dl > dd:last-child,
dl > dd:last-child > :last-child {
margin-bottom: 0;
Expand Down Expand Up @@ -738,6 +752,14 @@ abbr, acronym {
cursor: help;
}

.translated {
background-color: rgba(207, 255, 207, 0.2)
}

.untranslated {
background-color: rgba(255, 207, 207, 0.2)
}

/* -- code displays --------------------------------------------------------- */

pre {
Expand Down
2 changes: 1 addition & 1 deletion _static/css/theme.css

Large diffs are not rendered by default.

5 changes: 2 additions & 3 deletions _static/documentation_options.js
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
var DOCUMENTATION_OPTIONS = {
URL_ROOT: document.getElementById("documentation_options").getAttribute('data-url_root'),
VERSION: 'v1.18.2',
const DOCUMENTATION_OPTIONS = {
VERSION: '',
LANGUAGE: 'en',
COLLAPSE_INDEX: false,
BUILDER: 'html',
Expand Down
2 changes: 2 additions & 0 deletions _static/jquery.js

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions _static/pygments.css
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ span.linenos.special { color: #000000; background-color: #ffffc0; padding-left:
.highlight .cs { color: #3D7B7B; font-style: italic } /* Comment.Special */
.highlight .gd { color: #A00000 } /* Generic.Deleted */
.highlight .ge { font-style: italic } /* Generic.Emph */
.highlight .ges { font-weight: bold; font-style: italic } /* Generic.EmphStrong */
.highlight .gr { color: #E40000 } /* Generic.Error */
.highlight .gh { color: #000080; font-weight: bold } /* Generic.Heading */
.highlight .gi { color: #008400 } /* Generic.Inserted */
Expand Down
26 changes: 17 additions & 9 deletions _static/searchtools.js
Original file line number Diff line number Diff line change
Expand Up @@ -57,12 +57,12 @@ 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;

Expand All @@ -75,20 +75,24 @@ 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())
Expand All @@ -97,6 +101,9 @@ const _displayItem = (item, searchTerms) => {
listItem.appendChild(
Search.makeSearchSummary(data, searchTerms)
);
// 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);
};
Expand All @@ -115,14 +122,15 @@ const _finishSearch = (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
);
}
Expand Down Expand Up @@ -360,7 +368,7 @@ const Search = {
// console.info("search results:", Search.lastresults);

// print the results
_displayNextItem(results, results.length, searchTerms);
_displayNextItem(results, results.length, searchTerms, highlightTerms);
},

/**
Expand Down
16 changes: 13 additions & 3 deletions _static/sphinx_highlight.js
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down Expand Up @@ -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();
});
29 changes: 16 additions & 13 deletions about.html
Original file line number Diff line number Diff line change
@@ -1,20 +1,23 @@
<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<html class="writer-html5" lang="en" data-content_root="./">
<head>
<meta charset="utf-8" /><meta name="generator" content="Docutils 0.18.1: http://docutils.sourceforge.net/" />
<meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>About &mdash; Elpi v1.18.2 documentation</title>
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
<title>About &mdash; Elpi documentation</title>
<link rel="stylesheet" type="text/css" href="_static/pygments.css?v=80d5e7a1" />
<link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />


<!--[if lt IE 9]>
<script src="_static/js/html5shiv.min.js"></script>
<![endif]-->

<script src="https://ajax.googleapis.com/ajax/libs/jquery/3.6.0/jquery.min.js"></script>
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/sphinx_highlight.js"></script>
<script src="_static/jquery.js?v=5d32c60e"></script>
<script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
<script src="_static/documentation_options.js?v=5929fcd5"></script>
<script src="_static/doctools.js?v=888ff710"></script>
<script src="_static/sphinx_highlight.js?v=dc90522c"></script>
<script src="_static/js/theme.js"></script>
<link rel="author" title="About these documents" href="#" />
<link rel="index" title="Index" href="genindex.html" />
Expand Down Expand Up @@ -71,10 +74,10 @@
<div itemprop="articleBody">

<section id="about">
<h1>About<a class="headerlink" href="#about" title="Permalink to this heading"></a></h1>
<h1>About<a class="headerlink" href="#about" title="Link to this heading"></a></h1>
<p>This page is both an introspection and self documentation for this documentation stack.</p>
<section id="prerequisites">
<h2>Prerequisites<a class="headerlink" href="#prerequisites" title="Permalink to this heading"></a></h2>
<h2>Prerequisites<a class="headerlink" href="#prerequisites" title="Link to this heading"></a></h2>
<p>Before building this documentation, make sure to have <code class="docutils literal notranslate"><span class="pre">sphinx</span></code> installed:</p>
<div class="highlight-console notranslate"><div class="highlight"><pre><span></span><span class="go">pip install sphinx</span>
<span class="go">pip install in-place</span>
Expand All @@ -92,7 +95,7 @@ <h2>Prerequisites<a class="headerlink" href="#prerequisites" title="Permalink to
</div>
</section>
<section id="extensions">
<h2>Extensions<a class="headerlink" href="#extensions" title="Permalink to this heading"></a></h2>
<h2>Extensions<a class="headerlink" href="#extensions" title="Link to this heading"></a></h2>
<p>This documentation can make use of the following plugins:</p>
<div class="highlight-python notranslate"><div class="highlight"><pre><span></span><span class="n">extensions</span> <span class="o">=</span> <span class="p">[</span>
<span class="s1">&#39;sphinx.ext.intersphinx&#39;</span><span class="p">,</span>
Expand All @@ -103,7 +106,7 @@ <h2>Extensions<a class="headerlink" href="#extensions" title="Permalink to this
<p>Namely, <code class="docutils literal notranslate"><span class="pre">intersphinx</span></code> (<a class="reference external" href="https://www.sphinx-doc.org/en/master/usage/extensions/intersphinx.html">https://www.sphinx-doc.org/en/master/usage/extensions/intersphinx.html</a>) can generate links to the documentation of objects in external projects, either explicitly through the external role, or as a fallback resolution for any other cross-reference, and, <code class="docutils literal notranslate"><span class="pre">githubpages</span></code> (<a class="reference external" href="https://www.sphinx-doc.org/en/master/usage/extensions/githubpages.html#module-sphinx.ext.githubpages">https://www.sphinx-doc.org/en/master/usage/extensions/githubpages.html#module-sphinx.ext.githubpages</a>) which creates a <code class="docutils literal notranslate"><span class="pre">.nojekyll</span></code> file on generated HTML directory to publish the document on GitHub Pages.</p>
</section>
<section id="building">
<h2>Building<a class="headerlink" href="#building" title="Permalink to this heading"></a></h2>
<h2>Building<a class="headerlink" href="#building" title="Link to this heading"></a></h2>
<p><code class="docutils literal notranslate"><span class="pre">sphinx</span></code> comes with its own helpers to build the documentation but are not meant to be used directly, see <a class="reference internal" href="playground.html"><span class="doc">Playground</span></a> section for injection points.</p>
<p>Instead, use the <code class="docutils literal notranslate"><span class="pre">doc-sphinx</span></code> target of the source tree’s root’s <code class="docutils literal notranslate"><span class="pre">Makefile</span></code> to build the documentation:</p>
<div class="highlight-python notranslate"><div class="highlight"><pre><span></span><span class="n">make</span> <span class="n">doc</span><span class="o">-</span><span class="n">build</span>
Expand Down
Loading

0 comments on commit 6c8d70e

Please sign in to comment.