export/ 000755 000765 000024 00000000000 13014320007 012471 5 ustar 00gert staff 000000 000000 export/coq/ 000755 000765 000024 00000000000 13035504346 013270 5 ustar 00gert staff 000000 000000 export/Makefile 000644 000765 000024 00000000353 13014317667 014154 0 ustar 00gert staff 000000 000000 .PHONY : all coq html website clean all: coq html website html: $(MAKE) -C coq html coq: $(MAKE) -C coq website: $(MAKE) -C coq html mv coq/html/*html website rm -rf coq/html clean: $(MAKE) -C coq clean rm -f website/*html export/website/ 000755 000765 000024 00000000000 13035504346 014150 5 ustar 00gert staff 000000 000000 export/website/config.js 000644 000765 000024 00000002321 13014320007 015734 0 ustar 00gert staff 000000 000000 var coqdocjs = coqdocjs || {}; coqdocjs.repl = { "fun": "λ", "forall": "∀", "exists": "∃", "~": "¬", "/\\": "∧", "\\/": "∨", "->": "→", "<-": "←", "<->": "↔", "=>": "⇒", "<>": "≠", "<=": "≤", ">=": "≥", "el": "∈", "nel": "∉", "<<=": "⊆", "<<": "⊂", "|-": "⊢", "++": "⧺", "===": "≡", "=/=": "≢", "=~=": "≅", "==>": "⟹", "lhd": "⊲", "rhd": "⊳", "nat": "ℕ", "alpha": "α", "beta": "β", "gamma": "γ", "delta": "δ", "epsilon": "ε", "eta": "η", "iota": "ι", "kappa": "κ", "lambda": "λ", "mu": "μ", "nu": "ν", "omega": "ω", "phi": "ϕ", "pi": "π", "psi": "ψ", "rho": "ρ", "sigma": "σ", "tau": "τ", "theta": "θ", "xi": "ξ", "zeta": "ζ", "Delta": "Δ", "Gamma": "Γ", "Pi": "Π", "Sigma": "Σ", "Omega": "Ω", "Xi": "Ξ" }; coqdocjs.subscr = { "0" : "₀", "1" : "₁", "2" : "₂", "3" : "₃", "4" : "₄", "5" : "₅", "6" : "₆", "7" : "₇", "8" : "₈", "9" : "₉", }; coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="]; export/website/coqdoc.css 000644 000765 000024 00000005757 13014320007 016133 0 ustar 00gert staff 000000 000000 body{ font-family: 'Open Sans', sans-serif; font-size: 14px; color: #2D2D2D } a { text-decoration: none; border-radius: 3px; padding-left: 3px; padding-right: 3px; margin-left: -3px; margin-right: -3px; color: inherit; font-weight: bold; } #main .code a, #main .inlinecode a, #toc a { font-weight: inherit; } a[href]:hover, [clickable]:hover{ background-color: rgba(0,0,0,0.1); cursor: pointer; } h, h1, h2, h3, h4, h5 { line-height: 1; color: black; text-rendering: optimizeLegibility; font-weight: normal; letter-spacing: 0.1em; text-align: left; } div + br { display: none; } div:empty{ display: none;} #main h1 { font-size: 2em; } #main h2 { font-size: 1.667rem; } #main h3 { font-size: 1.333em; } #main h4, #main h5, #main h6 { font-size: 1em; } #toc h2 { padding-bottom: 0; } #main .doc { margin: 0; text-align: justify; } .inlinecode, .code, #main pre { font-family: monospace; } .code > br:first-child { display: none; } .doc + .code{ margin-top:0.5em; } .block{ display: block; margin-top: 5px; margin-bottom: 5px; padding: 10px; text-align: center; } .block img{ margin: 15px; } table.infrule { border: 0px; margin-left: 50px; margin-top: 10px; margin-bottom: 10px; } td.infrule { font-family: monospace; text-align: center; padding: 0; line-height: 1; } tr.infrulemiddle hr { margin: 1px 0 1px 0; } .infrulenamecol { color: rgb(60%,60%,60%); padding-left: 1em; padding-bottom: 0.1em } .id[type="constructor"], .id[type="projection"], .id[type="method"], .id[type="inductive"], .id[type="definition"], .id[type="abbreviation"], .id[title="constructor"], .id[title="projection"], .id[title="method"], .id[title="inductive"], .id[title="definition"], .id[title="abbreviation"] { color : #2874AE; } .id[type="var"], .id[type="variable"], .id[type="notation"], .id[title="var"], .id[title="variable"], .id[title="notation"] { color: inherit; } .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="library"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="library"] { color: inherit; } .id[type="lemma"], .id[title="lemma"] { color: #A30E16; } .id[type="keyword"], .id[title="keyword"]{ color: #188B0C; } .comment { color: #808080; } /* TOC */ #toc h2{ letter-spacing: 0; font-size: 1.333em; } /* Index */ #index { margin: 0; padding: 0; width: 100%; } #index #frontispiece { margin: 1em auto; padding: 1em; width: 60%; } .booktitle { font-size : 140% } .authors { font-size : 90%; line-height: 115%; } .moreauthors { font-size : 60% } #index #entrance { text-align: center; } #index #entrance .spacer { margin: 0 30px 0 30px; } ul.doclist { margin-top: 0em; margin-bottom: 0em; } #toc > * { clear: both; } #toc > a { display: block; float: left; margin-top: 1em; } #toc a h2{ display: inline; } export/website/coqdocjs.css 000644 000765 000024 00000006105 13014320007 016454 0 ustar 00gert staff 000000 000000 /* replace unicode */ .id[repl] .hidden { font-size: 0; } .id[repl]:before{ content: attr(repl); } /* folding proofs */ @keyframes show-proof { 0% { max-height: 1.2em; opacity: 1; } 99% { max-height: 1000em; } 100%{ } } @keyframes hide-proof { from { visibility: visible; max-height: 10em; opacity: 1; } to { max-height: 1.2em; } } .proof { cursor: pointer; } .proof * { cursor: pointer; } .proof { overflow: hidden; position: relative; transition: opacity 1s; display: inline-block; } .proof[show="false"] { max-height: 1.2em; visibility: hidden; opacity: 0; } .proof[show="false"][animate] { animation-name: hide-proof; animation-duration: 0.25s; } .proof[show=true] { animation-name: show-proof; animation-duration: 10s; } .proof[show="false"]:before { position: absolute; visibility: visible; width: 100%; height: 100%; display: block; opacity: 0; content: "M"; } .proof[show="false"]:hover:before { content: ""; } .proof[show="false"] + br + br { display: none; } .proof[show="false"]:hover { visibility: visible; opacity: 0.5; } #toggle-proofs[proof-status="no-proofs"] { display: none; } #toggle-proofs[proof-status="some-hidden"]:before { content: "Show Proofs"; } #toggle-proofs[proof-status="all-shown"]:before { content: "Hide Proofs"; } /* page layout */ html, body { height: 100%; margin:0; padding:0; } body { display: flex; flex-direction: column } #content { flex: 1; overflow: auto; display: flex; flex-direction: column; } #content:focus { outline: none; /* prevent glow in OS X */ } #main { display: block; padding: 16px; padding-top: 1em; padding-bottom: 2em; margin-left: auto; margin-right: auto; max-width: 60em; flex: 1 0 auto; } .libtitle { display: none; } /* header */ #header { width:100%; padding: 0; margin: 0; display: flex; align-items: center; background-color: rgb(21,57,105); color: white; font-weight: bold; overflow: hidden; } .button { cursor: pointer; } #header * { text-decoration: none; vertical-align: middle; margin-left: 15px; margin-right: 15px; } #header > .right, #header > .left { display: flex; flex: 1; align-items: center; } #header > .left { text-align: left; } #header > .right { flex-direction: row-reverse; } #header a, #header .button { color: white; box-sizing: border-box; } #header a { border-radius: 0; padding: 0.2em; } #header .button { background-color: rgb(63, 103, 156); border-radius: 1em; padding-left: 0.5em; padding-right: 0.5em; margin: 0.2em; } #header a:hover, #header .button:hover { background-color: rgb(181, 213, 255); color: black; } #header h1 { padding: 0; margin: 0;} /* footer */ #footer { text-align: center; opacity: 0.5; font-size: 75%; } /* hyperlinks */ @keyframes highlight { 50%{ background-color: black; } } :target * { animation-name: highlight; animation-duration: 1s; } a[name]:empty { float: right; } export/website/coqdocjs.js 000644 000765 000024 00000012006 13014320007 016275 0 ustar 00gert staff 000000 000000 var coqdocjs = coqdocjs || {}; (function(){ function replace(s){ var m; if (m = s.match(/^(.+)'/)) { return replace(m[1])+"'"; } else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) { return replace(m[1])+m[2].replace(/\d/g, function(d){return coqdocjs.subscr[d]}); } else if (coqdocjs.repl.hasOwnProperty(s)){ return coqdocjs.repl[s] } else { return s; } } function toArray(nl){ return Array.prototype.slice.call(nl); } function replInTextNodes() { coqdocjs.replInText.forEach(function(toReplace){ toArray(document.getElementsByClassName("code")).concat(toArray(document.getElementsByClassName("inlinecode"))).forEach(function(elem){ toArray(elem.childNodes).forEach(function(node){ if (node.nodeType != Node.TEXT_NODE) return; var fragments = node.textContent.split(toReplace); node.textContent = fragments[fragments.length-1]; for (var k = 0; k < fragments.length - 1; ++k) { node.parentNode.insertBefore(document.createTextNode(fragments[k]),node); var replacement = document.createElement("span"); replacement.appendChild(document.createTextNode(toReplace)); replacement.setAttribute("class", "id"); replacement.setAttribute("type", "keyword"); node.parentNode.insertBefore(replacement, node); } }); }); }); } function replNodes() { toArray(document.getElementsByClassName("id")).forEach(function(node){ if (["var", "variable", "keyword", "notation", "definition", "inductive"].indexOf(node.getAttribute("type"))>=0){ var text = node.textContent; var replText = replace(text); if(text != replText) { node.setAttribute("repl", replText); node.setAttribute("title", text); var hidden = document.createElement("span"); hidden.setAttribute("class", "hidden"); while (node.firstChild) { hidden.appendChild(node.firstChild); } node.appendChild(hidden); } } }); } function isProofStart(s){ return s == "Proof"; } function isProofEnd(s){ return ["Qed", "Admitted", "Defined"].indexOf(s) > -1; } function proofStatus(){ var proofs = toArray(document.getElementsByClassName("proof")); if(proofs.length) { for(proof of proofs) { if (proof.getAttribute("show") === "false") { return "some-hidden"; } } return "all-shown"; } else { return "no-proofs"; } } function updateView(){ document.getElementById("toggle-proofs").setAttribute("proof-status", proofStatus()); } function foldProofs() { toArray(document.getElementsByClassName("id")).forEach(function(node){ if(isProofStart(node.textContent)) { var proof = document.createElement("span"); proof.setAttribute("class", "proof"); node.parentNode.insertBefore(proof, node); if(proof.previousSibling.nodeType === Node.TEXT_NODE) proof.appendChild(proof.previousSibling); while(node && !isProofEnd(node.textContent)) { proof.appendChild(node); node = proof.nextSibling; } if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the Qed if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the dot after the Qed proof.addEventListener("click", function(proof){return function(e){ console.log(e.target.parentNode.tagName); if (e.target.parentNode.tagName.toLowerCase() === "a") return; proof.setAttribute("show", proof.getAttribute("show") === "true" ? "false" : "true"); proof.setAttribute("animate", ""); updateView(); };}(proof)); proof.setAttribute("show", "false"); } }); } function toggleProofs(){ var someProofsHidden = proofStatus() === "some-hidden"; toArray(document.getElementsByClassName("proof")).forEach(function(proof){ proof.setAttribute("show", someProofsHidden); proof.setAttribute("animate", ""); }); updateView(); } function repairDom(){ toArray(document.getElementsByClassName("id")).forEach(function(node){ node.setAttribute("type", node.getAttribute("title")); }); toArray(document.getElementsByClassName("idref")).forEach(function(ref){ toArray(ref.childNodes).forEach(function(child){ if (["var", "variable"].indexOf(child.getAttribute("type")) > -1) ref.removeAttribute("href"); }); }); } function fixTitle(){ var url = "/" + window.location.pathname; var modulename = "." + url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.')); modulename = modulename.substring(modulename.lastIndexOf('.')+1); if (modulename === "toc") {modulename = "Table of Contents";} else if (modulename === "indexpage") {modulename = "Index";} else {modulename = modulename + ".v";}; document.title = modulename; } function postprocess(){ repairDom(); replInTextNodes() replNodes(); foldProofs(); document.getElementById("toggle-proofs").addEventListener("click", toggleProofs); updateView(); } fixTitle(); document.addEventListener('DOMContentLoaded', postprocess); coqdocjs.toggleProofs = toggleProofs; })(); export/website/resources/ 000755 000765 000024 00000000000 13014320007 016145 5 ustar 00gert staff 000000 000000 export/website/resources/footer.html 000644 000765 000024 00000000274 13014320007 020334 0 ustar 00gert staff 000000 000000