From 3aecdb2c3fc849eebbf71a64ecff76008c80d5e5 Mon Sep 17 00:00:00 2001
From: Marco Perronet <perronet@mpi-sws.org>
Date: Mon, 18 Nov 2019 10:27:51 +0100
Subject: [PATCH] Update coqdocjs
... to get support for proofs started by `Next Obligation`.
---
scripts/coqdocjs/resources/coqdocjs.js | 58 +++++++++++++++++++-------
1 file changed, 43 insertions(+), 15 deletions(-)
diff --git a/scripts/coqdocjs/resources/coqdocjs.js b/scripts/coqdocjs/resources/coqdocjs.js
index 75ccbd272..10dc0bb65 100644
--- a/scripts/coqdocjs/resources/coqdocjs.js
+++ b/scripts/coqdocjs/resources/coqdocjs.js
@@ -6,7 +6,13 @@ function replace(s){
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]});
+ return replace(m[1])+m[2].replace(/\d/g, function(d){
+ if (coqdocjs.subscr.hasOwnProperty(d)) {
+ return coqdocjs.subscr[d];
+ } else {
+ return d;
+ }
+ });
} else if (coqdocjs.repl.hasOwnProperty(s)){
return coqdocjs.repl[s]
} else {
@@ -57,18 +63,29 @@ function replNodes() {
});
}
-function isProofStart(s){
- return s == "Proof";
+function isVernacStart(l, t){
+ t = t.trim();
+ for(var s of l){
+ if (t == s || t.startsWith(s+" ") || t.startsWith(s+".")){
+ return true;
+ }
+ }
+ return false;
+}
+
+function isProofStart(n){
+ return isVernacStart(["Proof"], n.textContent) ||
+ (isVernacStart(["Next"], n.textContent) && isVernacStart(["Obligation"], n.nextSibling.nextSibling.textContent));
}
function isProofEnd(s){
- return ["Qed", "Admitted", "Defined"].indexOf(s) > -1;
+ return isVernacStart(["Qed", "Admitted", "Defined", "Abort"], s);
}
function proofStatus(){
var proofs = toArray(document.getElementsByClassName("proof"));
if(proofs.length) {
- for(proof of proofs) {
+ for(var proof of proofs) {
if (proof.getAttribute("show") === "false") {
return "some-hidden";
}
@@ -85,8 +102,15 @@ function updateView(){
}
function foldProofs() {
- toArray(document.getElementsByClassName("id")).forEach(function(node){
- if(isProofStart(node.textContent)) {
+ var hasCommands = true;
+ var nodes = document.getElementsByClassName("command");
+ if(nodes.length == 0) {
+ hasCommands = false;
+ console.log("no command tags found")
+ nodes = document.getElementsByClassName("id");
+ }
+ toArray(nodes).forEach(function(node){
+ if(isProofStart(node)) {
var proof = document.createElement("span");
proof.setAttribute("class", "proof");
@@ -98,10 +122,9 @@ function foldProofs() {
node = proof.nextSibling;
}
if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the Qed
- if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the dot after the Qed
+ if (!hasCommands && 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");
@@ -123,6 +146,13 @@ function toggleProofs(){
}
function repairDom(){
+ // pull whitespace out of command
+ toArray(document.getElementsByClassName("command")).forEach(function(node){
+ while(node.firstChild && node.firstChild.textContent.trim() == ""){
+ console.log("try move");
+ node.parentNode.insertBefore(node.firstChild, node);
+ }
+ });
toArray(document.getElementsByClassName("id")).forEach(function(node){
node.setAttribute("type", node.getAttribute("title"));
});
@@ -137,12 +167,10 @@ function repairDom(){
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;
+ var basename = url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.'));
+ if (basename === "toc") {document.title = "Table of Contents";}
+ else if (basename === "indexpage") {document.title = "Index";}
+ else {document.title = basename;}
}
function postprocess(){
--
GitLab