Commit 3aecdb2c authored by Marco Perronet's avatar Marco Perronet Committed by Björn Brandenburg

Update coqdocjs

... to get support for proofs started by `Next Obligation`.
parent f4330fe0
......@@ -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(){
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment