Add coqdocjs for rendering better html

74af4a36 · Amin Timany · 2a75020b · 74af4a36 · 74af4a36 · 74af4a36
Commit 74af4a36 authored Jan 17, 2020 by Amin Timany
--- a/Makefile
+++ b/Makefile
+EXTRA_DIR:=coqdocjs/extra
+COQDOCFLAGS:= \
+  --toc --toc-depth 2 --html --interpolate \
+  --index indexpage --no-lib-name --parse-comments \
+  --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html
+export COQDOCFLAGS
+
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
 	+@make -f Makefile.coq $@

 all: Makefile.coq
 	+@make -f Makefile.coq all
-.PHONY: all
+
+html: Makefile.coq phony
+	rm -fr html
+	@$(MAKE) -f Makefile.coq html
+	cp $(EXTRA_DIR)/resources/* html
+
+.PHONY: all html

 clean: Makefile.coq
 	+@make -f Makefile.coq clean

--- a/coqdocjs/LICENSE
+++ b/coqdocjs/LICENSE
+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.
--- a/coqdocjs/extra/footer.html
+++ b/coqdocjs/extra/footer.html
+</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>
--- a/coqdocjs/extra/header.html
+++ b/coqdocjs/extra/header.html
+<!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">
--- a/coqdocjs/extra/resources/config.js
+++ b/coqdocjs/extra/resources/config.js
+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 = ["==>","<=>", "=>", "->", "<-", ":="];
--- a/coqdocjs/extra/resources/coqdoc.css
+++ b/coqdocjs/extra/resources/coqdoc.css
+@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;
+}
--- a/coqdocjs/extra/resources/coqdocjs.css
+++ b/coqdocjs/extra/resources/coqdocjs.css
+/* 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: visible;
+  opacity: 0.3;
+}
+
+.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;
+}
+
+@media only screen { /* no div with internal scrolling to allow printing of whole content */
+    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;
+}
+
+/* Proviola */
+
+div.code {
+  width: auto;
+  float: none;
+}
+
+div.goal {
+  position: fixed;
+  left: 75%;
+  width: 25%;
+  top: 3em;
+}
+
+div.doc {
+  clear: both;
+}
+
+span.command:hover {
+  background-color: inherit;
+}
--- a/coqdocjs/extra/resources/coqdocjs.js
+++ b/coqdocjs/extra/resources/coqdocjs.js
+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){