scripts/coqdocjs/resources/config.js

@@ -17,6 +17,7 @@ coqdocjs.repl = {
     "nel": "∉",
     "<<=": "⊆",
     "|-": "⊢",
+    ":=" : "≔",
     ">>": "»",
     "<<": "⊆",
     "++": "⧺",
@@ -53,7 +54,127 @@ coqdocjs.repl = {
     "Pi": "Π",
     "Sigma": "Σ",
     "Omega": "Ω",
-    "Xi": "Ξ"
+    "Xi": "Ξ",
+    // bold script capitals
+    // "A": "𝒜",
+    // "B": "ℬ",
+    // "C": "𝒞",
+    // "D": "𝒟",
+    // "E": "ℰ",
+    // "F": "ℱ",
+    // "G": "𝒢",
+    // "H": "ℋ",
+    // "I": "ℐ",
+    // "J": "𝒥",
+    // "K": "𝒦",
+    // "L": "ℒ",
+    // "M": "ℳ",
+    // "N": "𝒩",
+    // "O": "𝒪",
+    // "P": "𝒫",
+    // "Q": "𝒬",
+    // "R": "ℛ",
+    // "S": "𝒯",
+    // "T": "𝒯",
+    // "U": "𝒰",
+    // "V": "𝒱",
+    // "W": "𝒲",
+    // "X": "𝒳",
+    // "Y": "𝒴",
+    // "Z": "𝒵",
+    // bold italic captials
+    // "A": "𝑨",
+    // "B": "𝑩",
+    // "C": "𝑪",
+    // "D": "𝑫",
+    // "E": "𝑬",
+    // "F": "𝑭",
+    // "G": "𝑮",
+    // "H": "𝑯",
+    // "I": "𝑰",
+    // "J": "𝑱",
+    // "K": "𝑲",
+    // "L": "𝑳",
+    // "M": "𝑴",
+    // "N": "𝑵",
+    // "O": "𝑶",
+    // "P": "𝑷",
+    // "Q": "𝑸",
+    // "R": "𝑹",
+    // "S": "𝑺",
+    // "T": "𝑻",
+    // "U": "𝑼",
+    // "V": "𝑽",
+    // "W": "𝑾",
+    // "X": "𝑿",
+    // "Y": "𝒀",
+    // "Z": "𝒁",
+    // italic sans-serif captials
+    "A": "𝘈",
+    "B": "𝘉",
+    "C": "𝘊",
+    "D": "𝘋",
+    "E": "𝘌",
+    "F": "𝘍",
+    "G": "𝘎",
+    "H": "𝘏",
+    "I": "𝘐",
+    "J": "𝘑",
+    "K": "𝘒",
+    "L": "𝘓",
+    "M": "𝘔",
+    "N": "𝘕",
+    "O": "𝘖",
+    "P": "𝘗",
+    "Q": "𝘘",
+    "R": "𝘙",
+    "S": "𝘚",
+    "T": "𝘛",
+    "U": "𝘜",
+    "V": "𝘝",
+    "W": "𝘞",
+    "X": "𝘟",
+    "Y": "𝘠",
+    "Z": "𝘡",
+    // italic sans-serif lower-case letters
+    "a": "𝘢",
+    "b": "𝘣",
+    "c": "𝘤",
+    "d": "𝘥",
+    "e": "𝘦",
+    "f": "𝘧",
+    "g": "𝘨",
+    "h": "𝘩",
+    "i": "𝘪",
+    "j": "𝘫",
+    "k": "𝘬",
+    "l": "𝘭",
+    "m": "𝘮",
+    "n": "𝘯",
+    "o": "𝘰",
+    "p": "𝘱",
+    "q": "𝘲",
+    "r": "𝘳",
+    "s": "𝘴",
+    "t": "𝘵",
+    "u": "𝘶",
+    "v": "𝘷",
+    "w": "𝘸",
+    "x": "𝘹",
+    "y": "𝘺",
+    "z": "𝘻",
+    // MathComp syntax
+    "==": "⩵",
+    "!=": "≠",
+    "\\in": "∈",
+    "\\notin": "∉",
+    "\\sum_(": "∑(",
+    "\\prod_(": "∏(",
+    "\\cat_(": "⋃(",
+    "~~": "￢",
+    "'I_(": "𝕆(",
+    "&&": "⩑",
+    "||": "⩒",
 };
 
 coqdocjs.subscr = {
@@ -67,6 +188,27 @@ coqdocjs.subscr = {
   "7" : "₇",
   "8" : "₈",
   "9" : "₉",
+  "a" : "ₐ",
+  "e" : "ₑ",
+  "h" : "ₕ",
+  "i" : "ᵢ",
+  "j" : "ⱼ",
+  "k" : "ₖ",
+  "l" : "ₗ",
+  "m" : "ₘ",
+  "n" : "ₙ",
+  "o" : "ₒ",
+  "p" : "ₚ",
+  "r" : "ᵣ",
+  "s" : "ₛ",
+  "t" : "ₜ",
+  "u" : "ᵤ",
+  "v" : "ᵥ",
+  "x" : "ₓ",
+  // the below are currently not replaced
+  "+" : "₊",
+  "-" : "₋",
+  "=" : "₌",
 };
 
 coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="];

scripts/coqdocjs/resources/coqdoc.css

@@ -2,8 +2,8 @@
 @import url("fonts/inconsolata/font.css");
 
 body{
-    font-family: "Open Sans", serif;
-    font-size: 110%;
+    font-family: "Open Sans", sans-serif;
+    font-size: 17px;
     text-rendering: optimizeLegibility;
     color: #2D2D2D;
 }
@@ -29,6 +29,17 @@ a {
     font-weight: normal;
 }
 
+.doc-in-proof {
+    font-family: "Open Sans", sans-serif;
+    font-size: 17px;
+    padding-top: 0.5em;
+    margin-top: 0.5em;
+    padding-bottom: 0.5em;
+    margin-bottom: 0.5em;
+    border-top: 2px dashed #2874AE;
+    border-bottom: 2px dashed #2874AE;
+}
+
 #main .code a, #main .inlinecode a, #toc a {
     font-weight: inherit;
 }
@@ -82,9 +93,9 @@ div:empty{ display: none;}
     /* text-align: justify; */
 }
 
-.inlinecode, .code, #main pre {
+.inlinecode, .code, #main pre, #main code {
     font-family: "Inconsolata", monospace;
-    font-size: 110%;
+    font-size: 19px;
 }
 
 .code > br:first-child {

scripts/coqdocjs/resources/coqdocjs.js

 var coqdocjs = coqdocjs || {};
 (function(){
 
-function replace(s){
+function replace(s, letter_subscripts = true){
   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){
+  } else if (m = s.match(/^([A-Za-z_]*[A-Za-z]+)_?(\d+)$/)) {
+    return replace(m[1], false)+m[2].replace(/(\d)/g, function(d){
       if (coqdocjs.subscr.hasOwnProperty(d)) {
         return coqdocjs.subscr[d];
       } else {
         return d;
       }
     });
+  } else if (letter_subscripts
+             && (m = s.match(/^([A-Za-z_]*[A-Za-z]+)(_[aehijklmnoprstuvx])$/))) {
+    return replace(m[1], false)+m[2].replace(/_([aehijklmnoprstuvx])/g, function(d){
+      last = d[d.length - 1];
+      if (coqdocjs.subscr.hasOwnProperty(last)) {
+        return coqdocjs.subscr[last];
+      } else {
+        return d;
+      }
+    });
   } else if (coqdocjs.repl.hasOwnProperty(s)){
     return coqdocjs.repl[s]
   } else {
@@ -46,7 +56,7 @@ function replInTextNodes() {
 
 function replNodes() {
   toArray(document.getElementsByClassName("id")).forEach(function(node){
-    if (["var", "variable", "keyword", "notation", "definition", "inductive"].indexOf(node.getAttribute("type"))>=0){
+    if (["var", "variable", "keyword", "notation", "definition", "inductive", "binder"].indexOf(node.getAttribute("type"))>=0){
       var text = node.textContent;
       var replText = replace(text);
       if(text != replText) {
@@ -63,6 +73,65 @@ function replNodes() {
   });
 }
 
+function mergeAdjacentAnchorTags() {
+  // Step 1: Select all <a> elements
+  const aElements = Array.from(document.querySelectorAll("a"));
+
+  // Step 2: Process in reverse order to avoid disrupting the order of elements
+  for (let i = aElements.length - 1; i >= 0; i--) {
+    const a = aElements[i];
+
+    // Step 3: Check if this <a> has exactly one <span> child
+    if (a.children.length !== 1 || a.children[0].tagName !== "SPAN") continue;
+
+    const nextSibling = a.nextSibling;
+
+    // Step 4: Ensure the next sibling is an <a> element
+    if (!nextSibling || nextSibling.tagName !== "A") continue;
+
+    const nextA = nextSibling;
+
+    // Step 5: Check if the next <a> also has exactly one <span> child
+    if (nextA.children.length !== 1 || nextA.children[0].tagName !== "SPAN")
+      continue;
+
+    // Step 6: Check if href and class match
+    if (a.href !== nextA.href || a.className !== nextA.className) continue;
+
+    // Step 7: Extract and compare span attributes
+    const span1 = a.children[0];
+    const span2 = nextA.children[0];
+
+    const spanAttrsMatch =
+      span1.getAttribute("class") === span2.getAttribute("class") &&
+      span1.getAttribute("title") === span2.getAttribute("title") &&
+      span1.getAttribute("type") === span2.getAttribute("type");
+
+    if (!spanAttrsMatch) continue;
+
+    // Step 8: Create the new <a> element
+    const newA = document.createElement("a");
+    newA.href = a.href;
+    newA.className = a.className;
+
+    // Step 9: Create the new <span> with combined content
+    const newSpan = document.createElement("span");
+    newSpan.setAttribute("class", span1.getAttribute("class") || "");
+    newSpan.setAttribute("title", span1.getAttribute("title") || "");
+    newSpan.setAttribute("type", span1.getAttribute("type") || "");
+    newSpan.textContent = span1.textContent + span2.textContent;
+
+    newA.appendChild(newSpan);
+
+    // Step 10: Remove the original elements and insert the new one
+    const parent = a.parentNode;
+    parent.insertBefore(newA, nextA.nextSibling);
+    parent.removeChild(a);
+    parent.removeChild(nextA);
+  }
+}
+
+
 function isVernacStart(l, t){
   t = t.trim();
   for(var s of l){
@@ -82,6 +151,49 @@ function isProofEnd(s){
   return isVernacStart(["Qed", "Admitted", "Defined", "Abort"], s);
 }
 
+function eventuallyProofStart(node) {
+  while (node && !isProofStart(node)) {
+    node = node.nextSibling;
+  }
+  return node !== null;
+}
+
+function eventuallyProofEnd(node) {
+  while (node && !isProofEnd(node.textContent)) {
+    node = node.nextSibling;
+  }
+  return node !== null;
+}
+
+function mergeNextSibling(node) {
+  ns = node.nextSibling;
+  while (ns && (ns.nodeType != Node.ELEMENT_NODE || ns.firstChild === null)) {
+    ns = ns.nextSibling;
+  }
+  if (ns === null) {
+    return false;
+  }
+  if (ns.getAttribute("class") == "doc") {
+    /* fold comments interspersed in the proof into the given node */
+    ns.setAttribute("class", "doc-in-proof");
+    // node.appendChild(document.createElement("hr"));
+    node.appendChild(ns);
+    // node.appendChild(document.createElement("hr"));
+  } else if (
+    !eventuallyProofEnd(ns.firstChild) &&
+    eventuallyProofStart(ns.firstChild)
+  ) {
+    /* this doesn't look right, another proof is starting already */
+    return false;
+  } else {
+    /* merge next code block into node */
+    while (ns.firstChild) {
+      node.appendChild(ns.firstChild);
+    }
+  }
+  return true;
+}
+
 function proofStatus(){
   var proofs = toArray(document.getElementsByClassName("proof"));
   if(proofs.length) {
@@ -117,6 +229,13 @@ function foldProofs() {
       node.parentNode.insertBefore(proof, node);
       if(proof.previousSibling.nodeType === Node.TEXT_NODE)
         proof.appendChild(proof.previousSibling);
+
+      /* check if there are any comments interspersed with the proof */
+      while (
+        !eventuallyProofEnd(node) &&
+        mergeNextSibling(node.parentNode)
+      ) {}
+
       while(node && !isProofEnd(node.textContent)) {
         proof.appendChild(node);
         node = proof.nextSibling;
@@ -162,7 +281,7 @@ function repairDom(){
         ref.removeAttribute("href");
     });
   });
-
+  mergeAdjacentAnchorTags()
 }
 
 function fixTitle(){