My goal is to markup natural deduction proofs in HTML/CSS, similar to the following generated in LaTeX using the bussproofs package.
Notice how the bottom rule spans only the width of its immediate premises, rather than completely subsuming the preceding derivations.
I am unable to replicate this behavior in CSS:
function renderInferenceAsHtml(premises, consequent) {
const inferenceElement = document.createElement("div");
inferenceElement.dataset.inference = "";
const premisesElement = document.createElement("div");
premisesElement.dataset.premises = "";
for (const premise of premises) {
premisesElement.appendChild(premise);
}
const separatorElement = document.createElement("div");
separatorElement.dataset.separator = "";
inferenceElement.appendChild(premisesElement);
inferenceElement.appendChild(separatorElement);
inferenceElement.appendChild(consequent);
return inferenceElement;
}
function renderPropVarAsHtml(name) {
const element = document.createElement("i");
element.dataset.formula = "";
element.dataset.propVar = "";
element.textContent = name;
return element;
}
function renderTree(depth) {
const propVarName = String.fromCharCode(
"A".charCodeAt(0) + (depth - 1)
);
if (depth <= 1) {
return renderPropVarAsHtml(propVarName);
}
const left = renderTree(depth - 1);
const right = renderTree(depth - 1);
return renderInferenceAsHtml(
[left, right],
renderPropVarAsHtml(propVarName)
);
}
const treeHtml = renderTree(5);
document.body.appendChild(treeHtml);
[data-inference] {
display: flex;
flex-direction: column;
align-items: center;
width: max-content;
}
[data-premises] {
display: flex;
gap: 1em;
align-items: flex-end;
}
[data-separator] {
display: block;
height: 1px;
align-self: stretch;
background-color: currentColor;
margin: 0.2em 0;
}
[data-formula] {
line-height: 1;
}
Seeing as my working knowledge of CSS extends only to the box model, I see no obvious way to accomplish this without obfuscating the semantic structure of my HTML.
I am only looking for solutions that use pure HTML and CSS; I already have a JS solution.
I would consider a different markup by removing the separator and create it using CSS. I have a detailed article on how those border-image works: https://www.smashingmagazine.com/2024/01/css-border-image-property/
function renderInferenceAsHtml(premises, consequent) {
const inferenceElement = document.createElement("div");
inferenceElement.dataset.inference = "";
const premisesElement = document.createElement("div");
premisesElement.dataset.premises = "";
for (const premise of premises) {
premisesElement.appendChild(premise);
}
const separatorElement = document.createElement("div");
separatorElement.dataset.separator = "";
inferenceElement.appendChild(premisesElement);
/*inferenceElement.appendChild(separatorElement);*/
inferenceElement.appendChild(consequent);
return inferenceElement;
}
function renderPropVarAsHtml(name) {
const element = document.createElement("i");
element.dataset.formula = "";
element.dataset.propVar = "";
element.textContent = name;
return element;
}
function renderTree(depth) {
const propVarName = String.fromCharCode(
"A".charCodeAt(0) + (depth - 1)
);
if (depth <= 1) {
return renderPropVarAsHtml(propVarName);
}
const left = renderTree(depth - 1);
const right = renderTree(depth - 1);
return renderInferenceAsHtml(
[left, right],
renderPropVarAsHtml(propVarName)
);
}
const treeHtml = renderTree(5);
document.body.appendChild(treeHtml);
[data-inference] {
display: grid;
place-items: center;
gap: .2em;
width: max-content;
overflow: hidden; /* this one is important */
}
[data-premises] {
display: flex;
}
[data-formula] {
line-height: 1;
padding-bottom: .2em;
}
[data-inference]:first-child {padding-right: .5em}
[data-inference]:last-child {padding-left: .5em}
[data-premises]:not(:has([data-inference])) {
border-bottom: 1px solid;
gap: 1em;
}
[data-inference]:last-child:not(:first-child) > [data-prop-var] {
border-image: linear-gradient(0deg, currentColor 1px, #0000 0) fill 0 //0 0 0 100vw;
}
[data-inference]:first-child:not(:last-child) > [data-prop-var] {
border-image: linear-gradient(0deg, currentColor 1px, #0000 0) fill 0 //0 100vw 0 0;
}