Publish a scannable manual and a bibliography that links each paper back to the pages that use it.
Co-authored-by: Cursor <cursoragent@cursor.com>
This commit is contained in:
parent
cf8054a0b3
commit
695f8e84f7
45 changed files with 4848 additions and 338 deletions
130
doc/doc-extras.js
Normal file
130
doc/doc-extras.js
Normal file
|
|
@ -0,0 +1,130 @@
|
|||
(function () {
|
||||
function copyText(text, button) {
|
||||
var done = function () {
|
||||
var previous = button.textContent;
|
||||
button.textContent = "Copied";
|
||||
window.setTimeout(function () { button.textContent = previous; }, 1200);
|
||||
};
|
||||
if (navigator.clipboard && navigator.clipboard.writeText) {
|
||||
navigator.clipboard.writeText(text).then(done, function () {});
|
||||
return;
|
||||
}
|
||||
var area = document.createElement("textarea");
|
||||
area.value = text;
|
||||
document.body.appendChild(area);
|
||||
area.select();
|
||||
try { document.execCommand("copy"); done(); } catch (e) {}
|
||||
document.body.removeChild(area);
|
||||
}
|
||||
|
||||
document.querySelectorAll(".mwe-copy").forEach(function (button) {
|
||||
button.addEventListener("click", function () {
|
||||
var block = button.parentElement.querySelector("pre");
|
||||
if (!block) return;
|
||||
copyText(block.innerText.replace(/\n$/, ""), button);
|
||||
});
|
||||
});
|
||||
|
||||
// Sidebar order. Destinations match DoxygenLayout.xml, depth-first.
|
||||
var docPages = [
|
||||
["index.html", "Home"],
|
||||
["basics.html", "First program"],
|
||||
["which_dpf.html", "Pick a construction"],
|
||||
["guided_tour.html", "Guided tour"],
|
||||
["listings.html", "Code examples"],
|
||||
["input_type_examples.html", "Domain samples"],
|
||||
["output_type_examples.html", "Payload samples"],
|
||||
["evaluation_examples.html", "Evaluation samples"],
|
||||
["grotto_examples.html", "Grotto samples"],
|
||||
["iteratable_examples.html", "Iterable samples"],
|
||||
["capabilities.html", "Capabilities"],
|
||||
["verifiability.html", "Verifiability"],
|
||||
["programmability.html", "Programmability"],
|
||||
["comparisons.html", "Comparisons"],
|
||||
["multipoint_keys.html", "Multipoint"],
|
||||
["multiparty.html", "Multiparty"],
|
||||
["dealer_free.html", "Dealer-free keygen"],
|
||||
["beaver_triples.html", "Beaver triples"],
|
||||
["jet_and_ring.html", "Grotto"],
|
||||
["repr_and_twist.html", "Representation shift"],
|
||||
["ppvc_manual.html", "Programmable vectors"],
|
||||
["applications.html", "Application sketches"],
|
||||
["getting_started.html", "Manual"],
|
||||
["input_types.html", "Domains"],
|
||||
["output_types.html", "Payloads"],
|
||||
["evaluation.html", "Evaluation"],
|
||||
["iterables.html", "Iterables"],
|
||||
["api_reference.html", "Call index"],
|
||||
["namespaces.html", "Namespaces"],
|
||||
["annotated.html", "Class list"],
|
||||
["classes.html", "Class index"],
|
||||
["files.html", "File list"],
|
||||
["bibliography.html", "Bibliography"],
|
||||
["ideal_functionalities.html", "Ideal functionalities"],
|
||||
["changes.html", "Changelog"],
|
||||
["bugs.html", "Bugs"],
|
||||
["todo.html", "TODO"],
|
||||
["license.html", "License"],
|
||||
["authors.html", "Authors"],
|
||||
["submodules.html", "Submodules"]
|
||||
];
|
||||
|
||||
function currentPage() {
|
||||
var name = location.pathname.split("/").pop();
|
||||
if (!name || name === "") return "index.html";
|
||||
return name;
|
||||
}
|
||||
|
||||
function pageNav(kind) {
|
||||
var name = currentPage();
|
||||
var index = -1;
|
||||
for (var i = 0; i < docPages.length; i++) {
|
||||
if (docPages[i][0] === name) index = i;
|
||||
}
|
||||
if (index < 0) return null;
|
||||
var nav = document.createElement("nav");
|
||||
nav.className = "page-nav" + (kind === "bottom" ? " page-nav-bottom" : "");
|
||||
nav.setAttribute("aria-label", "Pages");
|
||||
function edge(text) {
|
||||
var span = document.createElement("span");
|
||||
span.className = "page-nav-edge";
|
||||
span.textContent = text;
|
||||
return span;
|
||||
}
|
||||
if (index > 0) {
|
||||
var back = document.createElement("a");
|
||||
back.href = docPages[index - 1][0];
|
||||
back.textContent = "\u2190 " + docPages[index - 1][1];
|
||||
nav.appendChild(back);
|
||||
} else {
|
||||
nav.appendChild(edge("\u2190"));
|
||||
}
|
||||
if (index + 1 < docPages.length) {
|
||||
var next = document.createElement("a");
|
||||
next.className = "page-nav-next";
|
||||
next.href = docPages[index + 1][0];
|
||||
next.textContent = docPages[index + 1][1] + " \u2192";
|
||||
nav.appendChild(next);
|
||||
} else {
|
||||
var done = edge("\u2192");
|
||||
done.className = "page-nav-edge page-nav-next";
|
||||
nav.appendChild(done);
|
||||
}
|
||||
return nav;
|
||||
}
|
||||
|
||||
function mountPageNav() {
|
||||
var contents = document.querySelector("#doc-content .contents") || document.querySelector(".contents");
|
||||
if (!contents || contents.querySelector(".page-nav")) return;
|
||||
var top = pageNav("top");
|
||||
if (!top) return;
|
||||
contents.insertBefore(top, contents.firstChild);
|
||||
contents.appendChild(pageNav("bottom"));
|
||||
}
|
||||
|
||||
if (document.readyState === "loading") {
|
||||
document.addEventListener("DOMContentLoaded", mountPageNav);
|
||||
} else {
|
||||
mountPageNav();
|
||||
}
|
||||
})();
|
||||
Loading…
Add table
Add a link
Reference in a new issue