diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1e15747ff708f6368eda20d203184f9914e551ae..68e72e5fc2ae4048bd286b7958a3240ad63544cc 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -60,15 +60,18 @@ doc:
dependencies:
- 1.9.0-coq-8.9
script:
- - make html
+ - make html -j ${NJOBS}
- mv html with-proofs
- - make gallinahtml
+ - make gallinahtml -j ${NJOBS}
- mv html without-proofs
+ - make htmlpretty -j ${NJOBS}
+ - mv html pretty
artifacts:
name: "prosa-spec-$CI_COMMIT_REF_NAME"
paths:
- "with-proofs/"
- "without-proofs/"
+ - "pretty/"
expire_in: 1 week
proof-length:
diff --git a/README.md b/README.md
index a110949c7ae6539891e766695a67810914f2139c..3ff34257c5a45a9dd7700c1c1dc06a79efd6a79a 100644
--- a/README.md
+++ b/README.md
@@ -45,7 +45,11 @@ For example, the schedulability analysis for global scheduling with release jitt
The Coqdoc documentation (as shown on the [webpage](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with `Make`:
-```$ make gallinahtml -j4```
+```$ make html -j 4``` *Documentation with proofs*
+
+```$ make gallinahtml -j 4``` *Documentation without proofs*
+
+```$ make htmlpretty -j 4``` *Pretty documentation (can also hide/show proofs)*
Since Coqdoc requires object files as input, please make sure that the code is compilable.
diff --git a/create_makefile.sh b/create_makefile.sh
index 114e18e6d5f1ba28b144c75769d7d9ce43b51014..f9ddace6ba1723261bd98f974406188d452f2329 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -36,3 +36,5 @@ else
sed -i 's|rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)|find . -name "*.vo" -delete -o -name "*.glob" -delete -o -name "*.v.d" -delete -o -name "*.vio" -delete -o -name "*.old" -delete -o -name "*.beautified" -delete|g' Makefile
fi
+# Patch Makefile.coqdocjs for pretty documentation targets
+printf "\n# Include pretty documentation targets\ninclude scripts/coqdocjs/Makefile.coqdocjs" >> Makefile
diff --git a/scripts/coqdocjs/Makefile.coqdocjs b/scripts/coqdocjs/Makefile.coqdocjs
new file mode 100644
index 0000000000000000000000000000000000000000..37f22596a79b34f14d103f6c5d31de560b61bdb0
--- /dev/null
+++ b/scripts/coqdocjs/Makefile.coqdocjs
@@ -0,0 +1,9 @@
+htmlpretty: $(GLOBFILES) $(VFILES)
+ $(SHOW)'COQDOC -d html $(GAL) --with-header scripts/coqdocjs/header.html --with-footer scripts/coqdocjs/footer.html'
+ $(HIDE)mkdir -p html
+ $(HIDE)$(COQDOC) \
+ -toc $(COQDOCFLAGS) \
+ --with-header scripts/coqdocjs/header.html --with-footer scripts/coqdocjs/footer.html \
+ -html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
+ $(HIDE)cp scripts/coqdocjs/resources/* html
+ $(HIDE)mv html/index.html html/indexpage.html
diff --git a/scripts/coqdocjs/footer.html b/scripts/coqdocjs/footer.html
new file mode 100644
index 0000000000000000000000000000000000000000..d0f79a884f0dc7f8f9a042947a56b6d561f8afa6
--- /dev/null
+++ b/scripts/coqdocjs/footer.html
@@ -0,0 +1,8 @@
+</div>
+<div id="footer">
+ Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
+</div>
+</div>
+</body>
+
+</html>
diff --git a/scripts/coqdocjs/header.html b/scripts/coqdocjs/header.html
new file mode 100644
index 0000000000000000000000000000000000000000..cc81721b4911be4187ac85cc7125b5c04175d40c
--- /dev/null
+++ b/scripts/coqdocjs/header.html
@@ -0,0 +1,27 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
+<script type="text/javascript" src="config.js"></script>
+<script type="text/javascript" src="coqdocjs.js"></script>
+</head>
+
+<body onload="document.getElementById('content').focus()">
+ <div id="header">
+ <span class="left">
+ <span class="modulename"> <script> document.write(document.title) </script> </span>
+ </span>
+
+ <span class="button" id="toggle-proofs"></span>
+
+ <span class="right">
+ <a href="../">Project Page</a>
+ <a href="./indexpage.html"> Index </a>
+ <a href="./toc.html"> Table of Contents </a>
+ </span>
+</div>
+ <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
+ <div id="main">
diff --git a/scripts/coqdocjs/resources/LICENSE b/scripts/coqdocjs/resources/LICENSE
new file mode 100644
index 0000000000000000000000000000000000000000..9cc94e573bb23ac1b5987be9e971960f0e862caf
--- /dev/null
+++ b/scripts/coqdocjs/resources/LICENSE
@@ -0,0 +1,21 @@
+Copyright (c) 2016, Tobias Tebbi
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+ * Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+ * Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/scripts/coqdocjs/resources/config.js b/scripts/coqdocjs/resources/config.js
new file mode 100644
index 0000000000000000000000000000000000000000..72be6131d5e48cdacabc115c366f3ad94ab00f74
--- /dev/null
+++ b/scripts/coqdocjs/resources/config.js
@@ -0,0 +1,72 @@
+var coqdocjs = coqdocjs || {};
+
+coqdocjs.repl = {
+ "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 = ["==>","<=>", "=>", "->", "<-", ":="];
diff --git a/scripts/coqdocjs/resources/coqdoc.css b/scripts/coqdocjs/resources/coqdoc.css
new file mode 100644
index 0000000000000000000000000000000000000000..b7accd6e96ddabd37fb143192567a34cd5a00817
--- /dev/null
+++ b/scripts/coqdocjs/resources/coqdoc.css
@@ -0,0 +1,197 @@
+@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700);
+
+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: "Droid Sans Mono", "DejaVu Sans Mono", 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[title="constructor"], .id[title="projection"], .id[title="method"] {
+ color: #A30E16;
+}
+
+.id[type="var"], .id[type="variable"],
+.id[title="var"], .id[title="variable"] {
+ color: inherit;
+}
+
+.id[type="definition"], .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="inductive"], .id[type="library"],
+.id[title="definition"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="inductive"], .id[title="library"] {
+ color: #A6650F;
+}
+
+.id[type="lemma"],
+.id[title="lemma"]{
+ color: #188B0C;
+}
+
+.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"],
+.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{
+ color : #2874AE;
+}
+
+.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;
+}
diff --git a/scripts/coqdocjs/resources/coqdocjs.css b/scripts/coqdocjs/resources/coqdocjs.css
new file mode 100644
index 0000000000000000000000000000000000000000..04244061654a9b7b60cc7844337270b7150335f1
--- /dev/null
+++ b/scripts/coqdocjs/resources/coqdocjs.css
@@ -0,0 +1,224 @@
+/* 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;
+}
diff --git a/scripts/coqdocjs/resources/coqdocjs.js b/scripts/coqdocjs/resources/coqdocjs.js
new file mode 100644
index 0000000000000000000000000000000000000000..75ccbd272970ba559c629814091602c73cbe92f8
--- /dev/null
+++ b/scripts/coqdocjs/resources/coqdocjs.js
@@ -0,0 +1,161 @@
+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;
+})();