From b681b735d3ba066b675e61a8a0b8af7ccd3888d0 Mon Sep 17 00:00:00 2001 From: zorkow Date: Tue, 7 Jul 2026 17:22:33 +0200 Subject: [PATCH 1/7] refactors bussproofs, implements some missing commands --- ts/input/tex/bussproofs/BussproofsItems.ts | 38 +++ ts/input/tex/bussproofs/BussproofsMappings.ts | 29 +- ts/input/tex/bussproofs/BussproofsMethods.ts | 310 +++++++++++------- 3 files changed, 245 insertions(+), 132 deletions(-) diff --git a/ts/input/tex/bussproofs/BussproofsItems.ts b/ts/input/tex/bussproofs/BussproofsItems.ts index a9a4f51ad..b9850c5b1 100644 --- a/ts/input/tex/bussproofs/BussproofsItems.ts +++ b/ts/input/tex/bussproofs/BussproofsItems.ts @@ -22,6 +22,7 @@ */ import TexError from '../TexError.js'; +import NodeUtil from '../NodeUtil.js'; import { BaseItem, CheckType, StackItem } from '../StackItem.js'; import { MmlNode } from '../../../core/MmlTree/MmlNode.js'; import Stack from '../Stack.js'; @@ -61,6 +62,13 @@ export class ProofTreeItem extends BaseItem { return [[this.factory.create('mml', node), item], true]; } if (item.isKind('stop')) { + if (this.getProperty('implicit')) { + throw new TexError( + 'MissingDisplayProof', + 'Missing %1 to display the proof tree.', + '\\DisplayProof' + ); + } throw new TexError('EnvMissingEnd', 'Missing \\end{%1}', this.getName()); } this.innerStack.Push(item); @@ -72,6 +80,7 @@ export class ProofTreeItem extends BaseItem { */ public toMml() { const tree = super.toMml(); + this.alignProof(tree); const start = this.innerStack.Top(); if (start.isKind('start') && !start.Size()) { return tree; @@ -80,4 +89,33 @@ export class ProofTreeItem extends BaseItem { const prefix = this.innerStack.Top().toMml(); return this.create('node', 'mrow', [prefix, tree], {}); } + + /** + * Adjusts the vertical alignment of the finished proof tree with respect + * to the baseline, as requested by \bottomAlignProof or \centerAlignProof. + * + * @param {MmlNode} tree The proof tree. + */ + private alignProof(tree: MmlNode) { + const align = this.getProperty('proofAlign') as string; + if (!align || align === 'normal') { + return; + } + const table = NodeUtil.isType(tree, 'mtable') + ? tree + : (tree.childNodes.find((node) => + NodeUtil.isType(node as MmlNode, 'mtable') + ) as MmlNode); + if (!table) { + return; + } + NodeUtil.setAttribute( + table, + 'align', + align === 'center' + ? 'center' + : // Align the baseline with that of the conclusion row. + `baseline ${this.getProperty('rootAtTop') ? 1 : 2}` + ); + } } diff --git a/ts/input/tex/bussproofs/BussproofsMappings.ts b/ts/input/tex/bussproofs/BussproofsMappings.ts index 586257654..565c57efc 100644 --- a/ts/input/tex/bussproofs/BussproofsMappings.ts +++ b/ts/input/tex/bussproofs/BussproofsMappings.ts @@ -37,29 +37,44 @@ new CommandMap('Bussproofs-macros', { QuinaryInfC: [BussproofsMethods.Inference, 5], RightLabel: [BussproofsMethods.Label, 'right'], LeftLabel: [BussproofsMethods.Label, 'left'], - // Abbreviations are automatically enabled + DisplayProof: BussproofsMethods.DisplayProof, + + // Abbreviations are automatically enabled, so this is a no-op. + EnableBpAbbreviations: BussproofsMethods.EnableAbbreviations, + AX: BussproofsMethods.AxiomF, AXC: BussproofsMethods.Axiom, + UI: [BussproofsMethods.InferenceF, 1], UIC: [BussproofsMethods.Inference, 1], + BI: [BussproofsMethods.InferenceF, 2], BIC: [BussproofsMethods.Inference, 2], + TI: [BussproofsMethods.InferenceF, 3], TIC: [BussproofsMethods.Inference, 3], + QI: [BussproofsMethods.InferenceF, 4], + QIC: [BussproofsMethods.Inference, 4], + QuI: [BussproofsMethods.InferenceF, 5], + QuIC: [BussproofsMethods.Inference, 5], RL: [BussproofsMethods.Label, 'right'], LL: [BussproofsMethods.Label, 'left'], + DP: BussproofsMethods.DisplayProof, + + kernHyps: BussproofsMethods.KernHyps, + insertBetweenHyps: BussproofsMethods.BetweenHyps, noLine: [BussproofsMethods.SetLine, 'none', false], singleLine: [BussproofsMethods.SetLine, 'solid', false], solidLine: [BussproofsMethods.SetLine, 'solid', false], dashedLine: [BussproofsMethods.SetLine, 'dashed', false], - // Not yet implemented in CSS! + dottedLine: [BussproofsMethods.SetLine, 'dotted', false], + // Double lines are not yet implemented in the output jax! // doubleLine: [BussproofsMethods.SetLine, 'double', false], - // dottedLine: [BussproofsMethods.SetLine, 'dotted', false], alwaysNoLine: [BussproofsMethods.SetLine, 'none', true], alwaysSingleLine: [BussproofsMethods.SetLine, 'solid', true], alwaysSolidLine: [BussproofsMethods.SetLine, 'solid', true], alwaysDashedLine: [BussproofsMethods.SetLine, 'dashed', true], - // Not yet implemented in CSS! + alwaysDottedLine: [BussproofsMethods.SetLine, 'dotted', true], + // Double lines are not yet implemented in the output jax! // alwaysDoubleLine: [BussproofsMethods.SetLine, 'double', true], - // alwaysDottedLine: [BussproofsMethods.SetLine, 'dotted', true], rootAtTop: [BussproofsMethods.RootAtTop, true], alwaysRootAtTop: [BussproofsMethods.RootAtTop, true], @@ -68,6 +83,10 @@ new CommandMap('Bussproofs-macros', { alwaysRootAtBottom: [BussproofsMethods.RootAtTop, false], // TODO: always commands should be persistent. + bottomAlignProof: [BussproofsMethods.AlignProof, 'bottom'], + centerAlignProof: [BussproofsMethods.AlignProof, 'center'], + normalAlignProof: [BussproofsMethods.AlignProof, 'normal'], + fCenter: BussproofsMethods.FCenter, Axiom: BussproofsMethods.AxiomF, UnaryInf: [BussproofsMethods.InferenceF, 1], diff --git a/ts/input/tex/bussproofs/BussproofsMethods.ts b/ts/input/tex/bussproofs/BussproofsMethods.ts index d3f5803b2..7d6544108 100644 --- a/ts/input/tex/bussproofs/BussproofsMethods.ts +++ b/ts/input/tex/bussproofs/BussproofsMethods.ts @@ -48,6 +48,30 @@ function paddedContent(parser: TexParser, content: string): MmlNode { return parser.create('node', 'mrow', [lpad, ...nodes, rpad]); } +/** + * Gets the current proof tree stack item. If the parser is not currently + * inside a prooftree environment, an implicit proof tree is started, which + * has to be terminated with a \DisplayProof command (as in the original + * plain TeX version of the package, where proof commands can occur anywhere + * in the text). + * + * @param {TexParser} parser The calling parser. + * @returns {StackItem} The (possibly newly created) proof tree item. + */ +function getProofTree(parser: TexParser): StackItem { + let top = parser.stack.Top(); + if (top.kind !== 'proofTree') { + top = parser.itemFactory.create('proofTree').setProperties({ + line: 'solid', + currentLine: 'solid', + rootAtTop: false, + implicit: true, + }); + parser.Push(top); + } + return top; +} + /** * Creates a ND style inference rule. * @@ -182,6 +206,91 @@ function parseFCenterLine(parser: TexParser, name: string): MmlNode { return table; } +/** + * Builds an inference rule from the topmost n elements of the proof tree. + * This implements the joint functionality of the InfC (plain conclusion) and + * Inf (sequent conclusion with \fCenter) commands of any arity. + * + * @param {TexParser} parser The current parser. + * @param {string} name The name of the calling command. + * @param {number} n Number of premises for this inference rule. + * @param {boolean} sequent True if the conclusion is a sequent line + * containing \fCenter. + */ +function doInference( + parser: TexParser, + name: string, + n: number, + sequent: boolean +) { + const top = getProofTree(parser); + if (top.Size() < n) { + throw new TexError('BadProofTree', 'Proof tree badly specified.'); + } + const rootAtTop = top.getProperty('rootAtTop') as boolean; + const childCount = n === 1 && !top.Peek()[0].childNodes.length ? 0 : n; + const hypSep = top.getProperty('hypSep') as string; + const children: MmlNode[] = []; + do { + if (children.length) { + // The separating column, possibly containing the material given by + // \insertBetweenHyps, which is parsed anew for each separator. + const sep = hypSep + ? [new TexParser(hypSep, parser.stack.env, parser.configuration).mml()] + : []; + children.unshift(parser.create('node', 'mtd', sep, {})); + } + children.unshift( + parser.create('node', 'mtd', [top.Pop()], { + rowalign: rootAtTop ? 'top' : 'bottom', + }) + ); + n--; + } while (n > 0); + const hypKern = top.getProperty('hypKern') as string; + if (hypKern) { + // \kernHyps: slide the block of hypotheses to the right (or left for + // negative values) by prepending a space to the first premise. + const mspace = parser.create('node', 'mspace', [], { width: hypKern }); + const mrow = children[0].childNodes[0] as MmlNode; + mspace.parent = mrow; + mrow.childNodes.unshift(mspace); + } + const row = parser.create('node', 'mtr', children, {}); + const table = parser.create( + 'node', + 'mtable', + [row], + hypSep + ? // The hypothesis separation replaces the default column spacing. + { framespacing: '0 0', columnspacing: '0em' } + : { framespacing: '0 0' } + ); + const conclusion = sequent + ? parseFCenterLine(parser, name) // TODO: Padding + : paddedContent(parser, parser.GetArgument(name)); + const style = top.getProperty('currentLine') as string; + if (style !== top.getProperty('line')) { + top.setProperty('currentLine', top.getProperty('line')); + } + const rule = createRule( + parser, + table, + [conclusion], + top.getProperty('left') as MmlNode, + top.getProperty('right') as MmlNode, + style, + rootAtTop + ); + top.setProperty('left', null); + top.setProperty('right', null); + top.setProperty('hypKern', null); + top.setProperty('hypSep', null); + BussproofsUtil.setProperty(rule, 'inference', childCount); + parser.configuration.addNode('inference', rule); + top.Push(rule); +} + // Namespace const BussproofsMethods: { [key: string]: ParseMethod } = { /** @@ -213,14 +322,7 @@ const BussproofsMethods: { [key: string]: ParseMethod } = { * @param {string} name The name of the command. */ Axiom(parser: TexParser, name: string) { - const top = parser.stack.Top(); - // TODO: Label error - if (top.kind !== 'proofTree') { - throw new TexError( - 'IllegalProofCommand', - 'Proof commands only allowed in prooftree environment.' - ); - } + const top = getProofTree(parser); const content = paddedContent(parser, parser.GetArgument(name)); BussproofsUtil.setProperty(content, 'axiom', true); top.Push(content); @@ -234,53 +336,7 @@ const BussproofsMethods: { [key: string]: ParseMethod } = { * @param {number} n Number of premises for this inference rule. */ Inference(parser: TexParser, name: string, n: number) { - const top = parser.stack.Top(); - if (top.kind !== 'proofTree') { - throw new TexError( - 'IllegalProofCommand', - 'Proof commands only allowed in prooftree environment.' - ); - } - if (top.Size() < n) { - throw new TexError('BadProofTree', 'Proof tree badly specified.'); - } - const rootAtTop = top.getProperty('rootAtTop') as boolean; - const childCount = n === 1 && !top.Peek()[0].childNodes.length ? 0 : n; - const children: MmlNode[] = []; - do { - if (children.length) { - children.unshift(parser.create('node', 'mtd', [], {})); - } - children.unshift( - parser.create('node', 'mtd', [top.Pop()], { - rowalign: rootAtTop ? 'top' : 'bottom', - }) - ); - n--; - } while (n > 0); - const row = parser.create('node', 'mtr', children, {}); - const table = parser.create('node', 'mtable', [row], { - framespacing: '0 0', - }); - const conclusion = paddedContent(parser, parser.GetArgument(name)); - const style = top.getProperty('currentLine') as string; - if (style !== top.getProperty('line')) { - top.setProperty('currentLine', top.getProperty('line')); - } - const rule = createRule( - parser, - table, - [conclusion], - top.getProperty('left') as MmlNode, - top.getProperty('right') as MmlNode, - style, - rootAtTop - ); - top.setProperty('left', null); - top.setProperty('right', null); - BussproofsUtil.setProperty(rule, 'inference', childCount); - parser.configuration.addNode('inference', rule); - top.Push(rule); + doInference(parser, name, n, false); }, /** @@ -291,14 +347,7 @@ const BussproofsMethods: { [key: string]: ParseMethod } = { * @param {string} side The side of the label. */ Label(parser: TexParser, name: string, side: string) { - const top = parser.stack.Top(); - // Label error - if (top.kind !== 'proofTree') { - throw new TexError( - 'IllegalProofCommand', - 'Proof commands only allowed in prooftree environment.' - ); - } + const top = getProofTree(parser); const content = ParseUtil.internalMath(parser, parser.GetArgument(name), 0); const label = content.length > 1 @@ -316,14 +365,7 @@ const BussproofsMethods: { [key: string]: ParseMethod } = { * @param {boolean} always Set as permanent style. */ SetLine(parser: TexParser, _name: string, style: string, always: boolean) { - const top = parser.stack.Top(); - // Label error - if (top.kind !== 'proofTree') { - throw new TexError( - 'IllegalProofCommand', - 'Proof commands only allowed in prooftree environment.' - ); - } + const top = getProofTree(parser); top.setProperty('currentLine', style); if (always) { top.setProperty('line', style); @@ -338,13 +380,7 @@ const BussproofsMethods: { [key: string]: ParseMethod } = { * @param {string} where If true root is at top, otherwise at bottom. */ RootAtTop(parser: TexParser, _name: string, where: boolean) { - const top = parser.stack.Top(); - if (top.kind !== 'proofTree') { - throw new TexError( - 'IllegalProofCommand', - 'Proof commands only allowed in prooftree environment.' - ); - } + const top = getProofTree(parser); top.setProperty('rootAtTop', where); }, @@ -355,13 +391,7 @@ const BussproofsMethods: { [key: string]: ParseMethod } = { * @param {string} name The name of the command. */ AxiomF(parser: TexParser, name: string) { - const top = parser.stack.Top(); - if (top.kind !== 'proofTree') { - throw new TexError( - 'IllegalProofCommand', - 'Proof commands only allowed in prooftree environment.' - ); - } + const top = getProofTree(parser); const line = parseFCenterLine(parser, name); BussproofsUtil.setProperty(line, 'axiom', true); top.Push(line); @@ -383,54 +413,80 @@ const BussproofsMethods: { [key: string]: ParseMethod } = { * @param {number} n Number of premises for this inference rule. */ InferenceF(parser: TexParser, name: string, n: number) { + doInference(parser, name, n, true); + }, + + /** + * Implements the DisplayProof command that terminates and displays a + * proof tree given outside of a prooftree environment. Inside the + * environment the command is redundant, as the display is provided by the + * end of the environment. + * + * @param {TexParser} parser The current parser. + * @param {string} _name The name of the command. + */ + DisplayProof(parser: TexParser, _name: string) { const top = parser.stack.Top(); if (top.kind !== 'proofTree') { - throw new TexError( - 'IllegalProofCommand', - 'Proof commands only allowed in prooftree environment.' - ); + throw new TexError('BadProofTree', 'Proof tree badly specified.'); } - if (top.Size() < n) { + if (!top.getProperty('implicit')) { + return; + } + if (top.Size() !== 1) { throw new TexError('BadProofTree', 'Proof tree badly specified.'); } - const rootAtTop = top.getProperty('rootAtTop') as boolean; - const childCount = n === 1 && !top.Peek()[0].childNodes.length ? 0 : n; - const children: MmlNode[] = []; - do { - if (children.length) { - children.unshift(parser.create('node', 'mtd', [], {})); - } - children.unshift( - parser.create('node', 'mtd', [top.Pop()], { - rowalign: rootAtTop ? 'top' : 'bottom', - }) - ); - n--; - } while (n > 0); - const row = parser.create('node', 'mtr', children, {}); - const table = parser.create('node', 'mtable', [row], { - framespacing: '0 0', - }); + const node = top.toMml(); + BussproofsUtil.setProperty(node, 'proof', true); + parser.stack.Pop(); + parser.Push(node); + }, - const conclusion = parseFCenterLine(parser, name); // TODO: Padding - const style = top.getProperty('currentLine') as string; - if (style !== top.getProperty('line')) { - top.setProperty('currentLine', top.getProperty('line')); - } - const rule = createRule( - parser, - table, - [conclusion], - top.getProperty('left') as MmlNode, - top.getProperty('right') as MmlNode, - style, - rootAtTop - ); - top.setProperty('left', null); - top.setProperty('right', null); - BussproofsUtil.setProperty(rule, 'inference', childCount); - parser.configuration.addNode('inference', rule); - top.Push(rule); + /** + * Implements the EnableBpAbbreviations command. The abbreviated commands + * are always enabled in this implementation, so this is a no-op. + * + * @param {TexParser} _parser The current parser. + * @param {string} _name The name of the command. + */ + EnableAbbreviations(_parser: TexParser, _name: string) {}, + + /** + * Implements the kernHyps command that slides the block of hypotheses of + * the next inference to the right by the given dimension (negative values + * slide to the left). + * + * @param {TexParser} parser The current parser. + * @param {string} name The name of the command. + */ + KernHyps(parser: TexParser, name: string) { + const top = getProofTree(parser); + top.setProperty('hypKern', parser.GetDimen(name)); + }, + + /** + * Implements the insertBetweenHyps command that provides the material + * separating the hypotheses of the next inference. + * + * @param {TexParser} parser The current parser. + * @param {string} name The name of the command. + */ + BetweenHyps(parser: TexParser, name: string) { + const top = getProofTree(parser); + top.setProperty('hypSep', parser.GetArgument(name)); + }, + + /** + * Implements the proof alignment commands that determine the vertical + * position of the proof tree with respect to the baseline. + * + * @param {TexParser} parser The current parser. + * @param {string} _name The name of the command. + * @param {string} align The alignment: 'bottom', 'center' or 'normal'. + */ + AlignProof(parser: TexParser, _name: string, align: string) { + const top = getProofTree(parser); + top.setProperty('proofAlign', align); }, }; From da7af36782773fc9691f14b2d34918252fb0f3ea Mon Sep 17 00:00:00 2001 From: zorkow Date: Tue, 7 Jul 2026 20:51:56 +0200 Subject: [PATCH 2/7] improves sequent alignment --- ts/input/tex/bussproofs/BussproofsUtil.ts | 92 ++++++++--------------- 1 file changed, 31 insertions(+), 61 deletions(-) diff --git a/ts/input/tex/bussproofs/BussproofsUtil.ts b/ts/input/tex/bussproofs/BussproofsUtil.ts index 701460b16..3d9607276 100644 --- a/ts/input/tex/bussproofs/BussproofsUtil.ts +++ b/ts/input/tex/bussproofs/BussproofsUtil.ts @@ -338,14 +338,17 @@ const adjustSequents = function (config: ParseOptions) { const premise = firstPremise( getPremises(inf, getProperty(inf, 'inferenceRule') as string) ); - const sequent = getProperty(premise, 'inferenceRule') - ? // If the first premise is an inference rule, check the conclusions for a sequent. - getConclusion( - premise, - getProperty(premise, 'inferenceRule') as string - ) - : // Otherwise it is a hyp and we have to check the formula itself. - premise; + // If the premise is an inference rule (possibly with labels), we have + // to check its conclusion for a sequent. Otherwise it is a hyp and we + // have to check the formula itself. + const rule = getProperty(premise, 'inferenceRule') + ? premise + : getProperty(premise, 'labelledRule') + ? getRule(premise) + : null; + const sequent = rule + ? getConclusion(rule, getProperty(rule, 'inferenceRule') as string) + : premise; if (getProperty(sequent, 'sequent')) { seq = sequent.childNodes[0]; collect.push(seq); @@ -353,7 +356,9 @@ const adjustSequents = function (config: ParseOptions) { } inf = premise; } - adjustSequentPairwise(config, collect); + if (collect.length > 1) { + alignSequents(config, collect); + } } }; @@ -387,73 +392,38 @@ const addSequentSpace = function ( }; /** - * Adjusts the sequent positioning for a list of inference rules by pairwise - * adjusting the width of formulas in sequents. I.e., + * Aligns the fCenter elements of a chain of sequents by padding the + * antecedent and succedent of each sequent to the maximal width occurring in + * the chain. As all sequent lines are centered within the proof tree, equal + * widths on both sides align the fCenter positions vertically. I.e., * A,B |- C * ------------ * A |- B,C * * will be adjusted to * - * A, B |- C + * A,B |- C__ * ---------------- - * A |- B,C + * __A |- B,C * * @param {ParseOptions} config Parser configuration options. * @param {MmlNode[]} sequents The list of sequents. */ -const adjustSequentPairwise = function ( - config: ParseOptions, - sequents: MmlNode[] -) { - let top = sequents.pop(); - while (sequents.length) { - const bottom = sequents.pop(); - const [left, right] = compareSequents(top, bottom); - if (getProperty(top.parent, 'axiom')) { - addSequentSpace( - config, - left < 0 ? top : bottom, - 0, - 'left', - Math.abs(left) - ); - addSequentSpace( - config, - right < 0 ? top : bottom, - 2, - 'right', - Math.abs(right) - ); +const alignSequents = function (config: ParseOptions, sequents: MmlNode[]) { + const lefts = sequents.map((seq) => getBBox(seq.childNodes[0] as MmlNode)); + const rights = sequents.map((seq) => getBBox(seq.childNodes[2] as MmlNode)); + const maxLeft = Math.max(...lefts); + const maxRight = Math.max(...rights); + for (let i = 0; i < sequents.length; i++) { + if (lefts[i] < maxLeft) { + addSequentSpace(config, sequents[i], 0, 'left', maxLeft - lefts[i]); + } + if (rights[i] < maxRight) { + addSequentSpace(config, sequents[i], 2, 'right', maxRight - rights[i]); } - top = bottom; } }; -/** - * Compares the top and bottom sequent of a inference rule - * Top: A |- B - * ---------- - * Bottom: C |- D - * - * @param {MmlNode} top Top sequent. - * @param {MmlNode} bottom Bottom sequent. - * @returns {[number, number]} The delta for left and right side of the sequents. - */ -const compareSequents = function ( - top: MmlNode, - bottom: MmlNode -): [number, number] { - const tr = getBBox(top.childNodes[2]); - const br = getBBox(bottom.childNodes[2]); - const tl = getBBox(top.childNodes[0]); - const bl = getBBox(bottom.childNodes[0]); - // Deltas - const dl = tl - bl; - const dr = tr - br; - return [dl, dr]; -}; - // For every inference rule we adjust the width of ruler by subtracting and // adding suitable spaces around the rule. The algorithm in detail. // From 9ebde931020f7baf05de51edb468fcc68a2dea01 Mon Sep 17 00:00:00 2001 From: zorkow Date: Tue, 7 Jul 2026 20:55:22 +0200 Subject: [PATCH 3/7] allow for double lines in CHTML output jax --- ts/input/tex/bussproofs/BussproofsMappings.ts | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/ts/input/tex/bussproofs/BussproofsMappings.ts b/ts/input/tex/bussproofs/BussproofsMappings.ts index 565c57efc..4c5bd07e7 100644 --- a/ts/input/tex/bussproofs/BussproofsMappings.ts +++ b/ts/input/tex/bussproofs/BussproofsMappings.ts @@ -65,16 +65,16 @@ new CommandMap('Bussproofs-macros', { solidLine: [BussproofsMethods.SetLine, 'solid', false], dashedLine: [BussproofsMethods.SetLine, 'dashed', false], dottedLine: [BussproofsMethods.SetLine, 'dotted', false], - // Double lines are not yet implemented in the output jax! - // doubleLine: [BussproofsMethods.SetLine, 'double', false], + // Double lines are not yet implemented in the SVG output jax! + doubleLine: [BussproofsMethods.SetLine, 'double', false], alwaysNoLine: [BussproofsMethods.SetLine, 'none', true], alwaysSingleLine: [BussproofsMethods.SetLine, 'solid', true], alwaysSolidLine: [BussproofsMethods.SetLine, 'solid', true], alwaysDashedLine: [BussproofsMethods.SetLine, 'dashed', true], alwaysDottedLine: [BussproofsMethods.SetLine, 'dotted', true], - // Double lines are not yet implemented in the output jax! - // alwaysDoubleLine: [BussproofsMethods.SetLine, 'double', true], + // Double lines are not yet implemented in the SVG output jax! + alwaysDoubleLine: [BussproofsMethods.SetLine, 'double', true], rootAtTop: [BussproofsMethods.RootAtTop, true], alwaysRootAtTop: [BussproofsMethods.RootAtTop, true], From 63ae55671bc855a0da988a72bb4c31f17f4bc39e Mon Sep 17 00:00:00 2001 From: zorkow Date: Tue, 7 Jul 2026 21:39:07 +0200 Subject: [PATCH 4/7] sequent tests for bussproofs --- testsuite/tests/input/tex/Bussproofs.test.ts | 181 +++++++++++++++++++ 1 file changed, 181 insertions(+) diff --git a/testsuite/tests/input/tex/Bussproofs.test.ts b/testsuite/tests/input/tex/Bussproofs.test.ts index dafa66cf4..5b3ba9e69 100644 --- a/testsuite/tests/input/tex/Bussproofs.test.ts +++ b/testsuite/tests/input/tex/Bussproofs.test.ts @@ -2,6 +2,7 @@ import { afterAll, beforeEach, describe, expect, it } from '@jest/globals'; import { getTokens, setupTexWithOutput, tex2mml } from '#helpers'; import '#js/input/tex/bussproofs/BussproofsConfiguration'; import '#js/input/tex/ams/AmsConfiguration'; +import '#js/input/tex/newcommand/NewcommandConfiguration'; beforeEach(() => setupTexWithOutput(['base', 'ams', 'bussproofs'])); @@ -213,4 +214,184 @@ describe('BussproofsRegProofs', () => { /**********************************************************************************/ +describe('BussproofsSequents', () => { + beforeEach(() => + setupTexWithOutput(['base', 'ams', 'newcommand', 'bussproofs']) + ); + + it('Sequent Axiom Only', () => { + expect( + tex2mml( + '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$A \\fCenter B$\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Sequent Axiom Display Proof No Space', () => { + expect(tex2mml('\\Axiom$A\\fCenterA$\\DisplayProof')).toMatchSnapshot(); + }); + + it('Sequent Unary', () => { + expect( + tex2mml( + '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$A,B \\fCenter C$\\UnaryInf$A \\fCenter B,C$\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Sequent Unary Chain', () => { + expect( + tex2mml( + '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$A,B,Q,R \\fCenter C$\\UnaryInf$A \\fCenter B,C$\\UnaryInf$\\fCenter A,B,C,D,E$\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Sequent Unary Chain Labelled', () => { + expect( + tex2mml( + '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$A,B,Q,R \\fCenter C$\\RightLabel{X}\\UnaryInf$A \\fCenter B,C$\\RightLabel{Y}\\UnaryInf$\\fCenter A,B,C$\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Sequent Unary Chain Plain Line', () => { + expect( + tex2mml( + '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$A,B \\fCenter C$\\UnaryInfC{intermediate}\\UnaryInf$A \\fCenter B,C,D,E$\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Sequent Unary Chain Binary Top', () => { + expect( + tex2mml( + '\\def\\fCenter{\\vdash}\\begin{prooftree}\\AxiomC{$P$}\\AxiomC{$Q$}\\BinaryInf$A,B,Q,R \\fCenter C$\\UnaryInf$A \\fCenter B,C$\\UnaryInf$\\fCenter A,B,C$\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Sequent Binary', () => { + expect( + tex2mml( + '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$\\fCenter A$\\Axiom$B \\fCenter C,D$\\UnaryInf$B,X,Y,Z \\fCenter C$\\BinaryInf$A,B \\fCenter C$\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Sequent Root At Top', () => { + expect( + tex2mml( + '\\def\\fCenter{\\vdash}\\begin{prooftree}\\rootAtTop\\Axiom$A,B,Q,R \\fCenter C$\\UnaryInf$A \\fCenter B,C$\\UnaryInf$\\fCenter A,B,C$\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Sequent Widest At Bottom', () => { + expect( + tex2mml( + '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$A \\fCenter B$\\UnaryInf$A,B \\fCenter C$\\UnaryInf$A,B,C,D \\fCenter E$\\UnaryInf$A,B,C,D,E,F \\fCenter G$\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Sequent Display Proof Chain', () => { + expect( + tex2mml( + '\\def\\fCenter{\\vdash}\\Axiom$A,B,Q \\fCenter C$\\UnaryInf$A \\fCenter B,C$\\UnaryInf$\\fCenter A,B,C$\\DP' + ) + ).toMatchSnapshot(); + }); + + it('Sequent Abbreviations', () => { + expect( + tex2mml( + '\\def\\fCenter{\\vdash}\\AX$A \\fCenter B$\\AX$C \\fCenter D$\\BI$E \\fCenter F$\\DP' + ) + ).toMatchSnapshot(); + }); +}); + +/**********************************************************************************/ + +describe('BussproofsCommands', () => { + it('Display Proof', () => { + expect(tex2mml('\\AxiomC{A}\\UnaryInfC{B}\\DisplayProof')).toMatchSnapshot(); + }); + + it('Display Proof Inline', () => { + expect(tex2mml('X = \\AxiomC{A}\\UnaryInfC{B}\\DP')).toMatchSnapshot(); + }); + + it('Enable Abbreviations', () => { + expect( + tex2mml('\\EnableBpAbbreviations\\AXC{A}\\AXC{B}\\AXC{C}\\TIC{D}\\DP') + ).toMatchSnapshot(); + }); + + it('Quaternary Abbreviation', () => { + expect( + tex2mml('\\AXC{A}\\AXC{B}\\AXC{C}\\AXC{D}\\QIC{E}\\DP') + ).toMatchSnapshot(); + }); + + it('Quinary Abbreviation', () => { + expect( + tex2mml('\\AXC{A}\\AXC{B}\\AXC{C}\\AXC{D}\\AXC{E}\\QuIC{F}\\DP') + ).toMatchSnapshot(); + }); + + it('Kern Hyps', () => { + expect( + tex2mml( + '\\begin{prooftree}\\AxiomC{A}\\AxiomC{B}\\kernHyps{1em}\\BinaryInfC{C}\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Insert Between Hyps', () => { + expect( + tex2mml( + '\\begin{prooftree}\\AxiomC{A}\\AxiomC{B}\\insertBetweenHyps{\\hskip 2em}\\BinaryInfC{C}\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Dotted Line', () => { + expect( + tex2mml( + '\\begin{prooftree}\\AxiomC{A}\\dottedLine\\UnaryInfC{B}\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Double Line', () => { + expect( + tex2mml( + '\\begin{prooftree}\\AxiomC{A}\\doubleLine\\UnaryInfC{B}\\end{prooftree}' + ) + ).toMatchSnapshot(); + }); + + it('Bottom Align Proof', () => { + expect( + tex2mml('\\bottomAlignProof\\AxiomC{A}\\UnaryInfC{B}\\DP') + ).toMatchSnapshot(); + }); + + it('Center Align Proof', () => { + expect( + tex2mml('\\centerAlignProof\\AxiomC{A}\\UnaryInfC{B}\\DP') + ).toMatchSnapshot(); + }); + + it('Normal Align Proof', () => { + expect( + tex2mml('\\normalAlignProof\\AxiomC{A}\\UnaryInfC{B}\\DP') + ).toMatchSnapshot(); + }); +}); + +/**********************************************************************************/ + afterAll(() => getTokens('bussproofs')); From d3435cfbe8f59aed0992784ba0a4be49f2727a47 Mon Sep 17 00:00:00 2001 From: zorkow Date: Tue, 7 Jul 2026 21:39:20 +0200 Subject: [PATCH 5/7] fix buggy handling of single sequent axiom --- ts/input/tex/bussproofs/BussproofsUtil.ts | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ts/input/tex/bussproofs/BussproofsUtil.ts b/ts/input/tex/bussproofs/BussproofsUtil.ts index 3d9607276..8d96cfcc7 100644 --- a/ts/input/tex/bussproofs/BussproofsUtil.ts +++ b/ts/input/tex/bussproofs/BussproofsUtil.ts @@ -328,7 +328,8 @@ const adjustSequents = function (config: ParseOptions) { } const collect = []; let inf = getParentInf(seq); - if (getProperty(inf, 'inference') !== 1) { + // An axiom-only proof has no parent inference rule. + if (!inf || getProperty(inf, 'inference') !== 1) { continue; } collect.push(seq); From e01f1c6b041993d74cd28ec2077d6fd794778c41 Mon Sep 17 00:00:00 2001 From: zorkow Date: Tue, 7 Jul 2026 21:59:25 +0200 Subject: [PATCH 6/7] update bussproofs test snapshot --- .../tex/__snapshots__/Bussproofs.test.ts.snap | 2812 +++++++++++++---- 1 file changed, 2127 insertions(+), 685 deletions(-) diff --git a/testsuite/tests/input/tex/__snapshots__/Bussproofs.test.ts.snap b/testsuite/tests/input/tex/__snapshots__/Bussproofs.test.ts.snap index 78e77a56a..f37b175ff 100644 --- a/testsuite/tests/input/tex/__snapshots__/Bussproofs.test.ts.snap +++ b/testsuite/tests/input/tex/__snapshots__/Bussproofs.test.ts.snap @@ -1,8 +1,8 @@ // Jest Snapshot v1, https://goo.gl/fbAQLP -exports[`BussproofsRegInf Binary Inference 1`] = ` -" - +exports[`BussproofsCommands Bottom Align Proof 1`] = ` +" + @@ -14,11 +14,34 @@ exports[`BussproofsRegInf Binary Inference 1`] = ` - + + + + + + + + + B + + + + + +" +`; + +exports[`BussproofsCommands Center Align Proof 1`] = ` +" + + + + + - + - B + A @@ -30,7 +53,7 @@ exports[`BussproofsRegInf Binary Inference 1`] = ` - C + B @@ -39,9 +62,135 @@ exports[`BussproofsRegInf Binary Inference 1`] = ` " `; -exports[`BussproofsRegInf Binary Inference Abbr 1`] = ` -" - +exports[`BussproofsCommands Display Proof 1`] = ` +" + + + + + + + + + A + + + + + + + + + + + + B + + + + + +" +`; + +exports[`BussproofsCommands Display Proof Inline 1`] = ` +" + X + = + + + + + + + + + A + + + + + + + + + + + + B + + + + + +" +`; + +exports[`BussproofsCommands Dotted Line 1`] = ` +" + + + + + + + + + A + + + + + + + + + + + + B + + + + + +" +`; + +exports[`BussproofsCommands Double Line 1`] = ` +" + + + + + + + + + A + + + + + + + + + + + + B + + + + + +" +`; + +exports[`BussproofsCommands Enable Abbreviations 1`] = ` +" + @@ -61,6 +210,14 @@ exports[`BussproofsRegInf Binary Inference Abbr 1`] = ` + + + + + C + + + @@ -69,7 +226,7 @@ exports[`BussproofsRegInf Binary Inference Abbr 1`] = ` - C + D @@ -78,253 +235,127 @@ exports[`BussproofsRegInf Binary Inference Abbr 1`] = ` " `; -exports[`BussproofsRegInf Label Both 1`] = ` -" - - - - L - - - - - - - - - - - A - - - - - - - - - - - - B - - - - - - - - R - - - +exports[`BussproofsCommands Insert Between Hyps 1`] = ` +" + + + + + + + + + A + + + + + + + + + + B + + + + + + + + + + + + C + + + + + " `; -exports[`BussproofsRegInf Label Both Abbr 1`] = ` -" - - - - L - - - - - - - - - - - A - - - - - - - - - - - - B - - - - - - - - R - - - -" -`; - -exports[`BussproofsRegInf Label Left 1`] = ` -" - - - - L - - - - - - - - - - - A - - - - - - - - - - - - B - - - - - - -" -`; - -exports[`BussproofsRegInf Label Left Abbr 1`] = ` -" - - - - L - - - - - - - - - - - A - - - - - - - - - - - - B - - - - - - -" -`; - -exports[`BussproofsRegInf Label Right 1`] = ` -" - - - - - - - - - - A - - - - - - - - - - - - B - - - - - - - - R - - - +exports[`BussproofsCommands Kern Hyps 1`] = ` +" + + + + + + + + + + A + + + + + + + + B + + + + + + + + + + + + C + + + + + " `; -exports[`BussproofsRegInf Label Right Abbr 1`] = ` -" - - - - - - - - - - A - - - - - - - - - - - - B - - - - - - - - R - - - +exports[`BussproofsCommands Normal Align Proof 1`] = ` +" + + + + + + + + + A + + + + + + + + + + + + B + + + + + " `; -exports[`BussproofsRegInf Quaternary Inference 1`] = ` -" - +exports[`BussproofsCommands Quaternary Abbreviation 1`] = ` +" + - + A @@ -332,7 +363,7 @@ exports[`BussproofsRegInf Quaternary Inference 1`] = ` - + B @@ -340,7 +371,7 @@ exports[`BussproofsRegInf Quaternary Inference 1`] = ` - + C @@ -348,7 +379,7 @@ exports[`BussproofsRegInf Quaternary Inference 1`] = ` - + D @@ -371,15 +402,15 @@ exports[`BussproofsRegInf Quaternary Inference 1`] = ` " `; -exports[`BussproofsRegInf Quinary Inference 1`] = ` -" - +exports[`BussproofsCommands Quinary Abbreviation 1`] = ` +" + - + A @@ -387,7 +418,7 @@ exports[`BussproofsRegInf Quinary Inference 1`] = ` - + B @@ -395,7 +426,7 @@ exports[`BussproofsRegInf Quinary Inference 1`] = ` - + C @@ -403,7 +434,7 @@ exports[`BussproofsRegInf Quinary Inference 1`] = ` - + D @@ -411,7 +442,7 @@ exports[`BussproofsRegInf Quinary Inference 1`] = ` - + E @@ -434,33 +465,9 @@ exports[`BussproofsRegInf Quinary Inference 1`] = ` " `; -exports[`BussproofsRegInf Single Axiom 1`] = ` -" - - - - A - - - -" -`; - -exports[`BussproofsRegInf Single Axiom Abbr 1`] = ` -" - - - - A - - - -" -`; - -exports[`BussproofsRegInf Trinary Inference 1`] = ` -" - +exports[`BussproofsRegInf Binary Inference 1`] = ` +" + @@ -480,14 +487,6 @@ exports[`BussproofsRegInf Trinary Inference 1`] = ` - - - - - C - - - @@ -496,7 +495,7 @@ exports[`BussproofsRegInf Trinary Inference 1`] = ` - D + C @@ -505,9 +504,9 @@ exports[`BussproofsRegInf Trinary Inference 1`] = ` " `; -exports[`BussproofsRegInf Trinary Inference Abbr 1`] = ` -" - +exports[`BussproofsRegInf Binary Inference Abbr 1`] = ` +" + @@ -527,14 +526,6 @@ exports[`BussproofsRegInf Trinary Inference Abbr 1`] = ` - - - - - C - - - @@ -543,7 +534,7 @@ exports[`BussproofsRegInf Trinary Inference Abbr 1`] = ` - D + C @@ -552,151 +543,625 @@ exports[`BussproofsRegInf Trinary Inference Abbr 1`] = ` " `; -exports[`BussproofsRegInf Unary Inference 1`] = ` -" - - - - - - - - - A - - - - - - - - - - - - B - - - - - +exports[`BussproofsRegInf Label Both 1`] = ` +" + + + + L + + + + + + + + + + + A + + + + + + + + + + + + B + + + + + + + + R + + + " `; -exports[`BussproofsRegInf Unary Inference Abbr 1`] = ` -" - - - - - - - - - A - - - - - - - - - - - - B - - - - - +exports[`BussproofsRegInf Label Both Abbr 1`] = ` +" + + + + L + + + + + + + + + + + A + + + + + + + + + + + + B + + + + + + + + R + + + " `; -exports[`BussproofsRegProofs Extreme 1`] = ` -" - - - - - BBB - - - - - - - - - - - - - WWW - - - - - - - - - - - HHHHH - - - - - - - - - - D - - - - - - - - A1 - - - - - - - - A2 - - - - - - - - - - - - Q - - - - - - - 11111111111111111 - - - - - - - +exports[`BussproofsRegInf Label Left 1`] = ` +" + + + + L + + + + + + + + + + + A + + + + + + + + + + + + B + + + + + + +" +`; + +exports[`BussproofsRegInf Label Left Abbr 1`] = ` +" + + + + L + + + + + + + + + + + A + + + + + + + + + + + + B + + + + + + +" +`; + +exports[`BussproofsRegInf Label Right 1`] = ` +" + + + + + + + + + + A + + + + + + + + + + + + B + + + + + + + + R + + + +" +`; + +exports[`BussproofsRegInf Label Right Abbr 1`] = ` +" + + + + + + + + + + A + + + + + + + + + + + + B + + + + + + + + R + + + +" +`; + +exports[`BussproofsRegInf Quaternary Inference 1`] = ` +" + + + + + + + + + A + + + + + + + + B + + + + + + + + C + + + + + + + + D + + + + + + + + + + + + E + + + + + +" +`; + +exports[`BussproofsRegInf Quinary Inference 1`] = ` +" + + + + + + + + + A + + + + + + + + B + + + + + + + + C + + + + + + + + D + + + + + + + + E + + + + + + + + + + + + F + + + + + +" +`; + +exports[`BussproofsRegInf Single Axiom 1`] = ` +" + + + + A + + + +" +`; + +exports[`BussproofsRegInf Single Axiom Abbr 1`] = ` +" + + + + A + + + +" +`; + +exports[`BussproofsRegInf Trinary Inference 1`] = ` +" + + + + + + + + + A + + + + + + + + B + + + + + + + + C + + + + + + + + + + + + D + + + + + +" +`; + +exports[`BussproofsRegInf Trinary Inference Abbr 1`] = ` +" + + + + + + + + + A + + + + + + + + B + + + + + + + + C + + + + + + + + + + + + D + + + + + +" +`; + +exports[`BussproofsRegInf Unary Inference 1`] = ` +" + + + + + + + + + A + + + + + + + + + + + + B + + + + + +" +`; + +exports[`BussproofsRegInf Unary Inference Abbr 1`] = ` +" + + + + + + + + + A + + + + + + + + + + + + B + + + + + +" +`; + +exports[`BussproofsRegProofs Extreme 1`] = ` +" + + + + + BBB + + + + + + + + + + + + + WWW + + + + + + + + + + + HHHHH + + + + + + + + + + D + + + + + + + + A1 + + + + + + + + A2 + + + + + + + + + + + + Q + + + + + + + 11111111111111111 + + + + + + + BBBB @@ -2255,7 +2720,216 @@ exports[`BussproofsRegProofs Simple Proofs Left Labels 1`] = ` - + + + + + + M + + + + + + + + + + + + + N + → + R + + + + + + + + +" +`; + +exports[`BussproofsRegProofs Simple Proofs Mixed Labels 1`] = ` +" + + + + + DD + + + + + + + + + + + + + CCCCC + + + + + + + + + + + + + + + + + D + + + + + + + + A1 + + + + + + + + A2 + + + + + + + + + + + + Q + + + + + + + + + + + + + BBB + + + + + + + + + + A + + + + + + + + + + + + + + + + B + + + + + + + + R + + + + + + + + + + + + + C + → + D + → + Q + + + + + + + + AAAA + + + + + + + + + + + + + E + + + + + + + + + + + + + + + + + F + + + + + + + + + + + @@ -2282,32 +2956,29 @@ exports[`BussproofsRegProofs Simple Proofs Left Labels 1`] = ` + + + QERE + + " `; -exports[`BussproofsRegProofs Simple Proofs Mixed Labels 1`] = ` -" - - - - - DD - - +exports[`BussproofsRegProofs Simple Proofs Right Labels 1`] = ` +" + + - - - - - CCCCC - + + + @@ -2361,11 +3032,8 @@ exports[`BussproofsRegProofs Simple Proofs Mixed Labels 1`] = ` - - - - BBB - + + @@ -2381,7 +3049,7 @@ exports[`BussproofsRegProofs Simple Proofs Mixed Labels 1`] = ` - + @@ -2442,6 +3110,9 @@ exports[`BussproofsRegProofs Simple Proofs Mixed Labels 1`] = ` + + BBB + @@ -2451,26 +3122,867 @@ exports[`BussproofsRegProofs Simple Proofs Mixed Labels 1`] = ` - - - F - - + + + F + + + + + + + CCCCC + + + + + + + + + + + + M + + + + + + + + + + + + + N + → + R + + + + + + + + + QERE + + + + +" +`; + +exports[`BussproofsSequents Sequent Abbreviations 1`] = ` +" + + + + + + + + + + A + + + ⊢ + + + B + + + + + + + + + + C + + + ⊢ + + + D + + + + + + + + + + + + + + E + + + ⊢ + + + F + + + + + + +" +`; + +exports[`BussproofsSequents Sequent Axiom Display Proof No Space 1`] = ` +" + + + + A + + + + A + + + +" +`; + +exports[`BussproofsSequents Sequent Axiom Only 1`] = ` +" + + + + A + + + ⊢ + + + B + + + +" +`; + +exports[`BussproofsSequents Sequent Binary 1`] = ` +" + + + + + + + + + + + ⊢ + + + A + + + + + + + + + + + + + + + + + B + + + ⊢ + + + C + , + D + + + + + + + + + + + + + + B + , + X + , + Y + , + Z + + + ⊢ + + + C + + + + + + + + + + + + + + + + + + A + , + B + + + ⊢ + + + C + + + + + + +" +`; + +exports[`BussproofsSequents Sequent Display Proof Chain 1`] = ` +" + + + + + + + + + + + + + + + + A + , + B + , + Q + + + ⊢ + + + C + + + + + + + + + + + + + + + + A + + + ⊢ + + + B + , + C + + + + + + + + + + + + + + + + + + + + + ⊢ + + + A + , + B + , + C + + + + + + +" +`; + +exports[`BussproofsSequents Sequent Root At Top 1`] = ` +" + + + + + + + + + + ⊢ + + + A + , + B + , + C + + + + + + + + + + + + + + + + + + A + + + ⊢ + + + B + , + C + + + + + + + + + + + + + + + A + , + B + , + Q + , + R + + + ⊢ + + + C + + + + + + + + + + + + + + + + +" +`; + +exports[`BussproofsSequents Sequent Unary 1`] = ` +" + + + + + + + + + + A + , + B + + + ⊢ + + + C + + + + + + + + + + + + + + + + A + + + ⊢ + + + B + , + C + + + + + + +" +`; + +exports[`BussproofsSequents Sequent Unary Chain 1`] = ` +" + + + + + + + + + + + + + + + + + + A + , + B + , + Q + , + R + + + ⊢ + + + C + + + + + + + + + + + + + + + + A + + + ⊢ + + + B + , + C + - - + + + + + + + + + + + + + + + + + + ⊢ + + + A + , + B + , + C + , + D + , + E + + + + + + + +" +`; + +exports[`BussproofsSequents Sequent Unary Chain Binary Top 1`] = ` +" + + + + + + + + + + + + + + + + + + + + + + P + + + + + + + + + + Q + + + + + + + + + + + + + + A + , + B + , + Q + , + R + + + ⊢ + + + C + + + + + + + + + + + + + + + + + + + A + + + ⊢ + + + B + , + C + + + + + + + + + + + + + + + + + + + + + ⊢ + + + A + , + B + , + C + + + + + + +" +`; + +exports[`BussproofsSequents Sequent Unary Chain Labelled 1`] = ` +" + + + + + + + + + + + + + + + + + + + A + , + B + , + Q + , + R + + + ⊢ + + + C + + + + + + + + + + + + + + + + A + + + ⊢ + + + B + , + C + + + + + + + + + X + - - - - + + + + + + + + + + + + + + + ⊢ + + + A + , + B + , + C + + + + + + + + + Y + + + +" +`; + +exports[`BussproofsSequents Sequent Unary Chain Plain Line 1`] = ` +" + + + + + + + - - - M - + + + + + + + + + + + A + , + B + + + ⊢ + + + C + + + + + + + + + + + + + + intermediate + + + + + @@ -2479,233 +3991,163 @@ exports[`BussproofsRegProofs Simple Proofs Mixed Labels 1`] = ` - - - - N - → - R - - - + + + + + A + + + ⊢ + + + B + , + C + , + D + , + E + + + - - - QERE - - " `; -exports[`BussproofsRegProofs Simple Proofs Right Labels 1`] = ` -" - - - - - - - - - - - - +exports[`BussproofsSequents Sequent Widest At Bottom 1`] = ` +" + + + + + + + + + + + + - - + + - - - - - - - - - - - D - - - - - - - - A1 - - - - - - - - A2 - - - - - - - - - - - - Q - - - - - - + + + + + + + + + A + + + ⊢ + + + B + + + + + + + - - - - - - - - - - - - - A - - - - - - - - - - - - - - - - B - - - - - - - - R - - - - - - - - - - - - - C - → - D - → - Q - - - - - - - - AAAA - - - - - - - - - - - - - E - - - - - - - BBB - - - + + + + + + + + A + , + B + + + ⊢ + + + C + + + + + + + + + + - - - F - - + + A + , + B + , + C + , + D + + + ⊢ + + + E + - - CCCCC - - - - - - - - - - - - M - - - - - - - - - - - - - N - → - R - - - - - - - - - QERE - - - + + + + + + + + + + + + + + + A + , + B + , + C + , + D + , + E + , + F + + + ⊢ + + + G + + + + + + " `; From 27bfcf7d919f0133ee3d65d3358c3863a3c076cb Mon Sep 17 00:00:00 2001 From: zorkow Date: Tue, 14 Jul 2026 11:43:04 +0200 Subject: [PATCH 7/7] incorporate review suggestions --- ts/input/tex/bussproofs/BussproofsItems.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ts/input/tex/bussproofs/BussproofsItems.ts b/ts/input/tex/bussproofs/BussproofsItems.ts index b9850c5b1..c45ac334a 100644 --- a/ts/input/tex/bussproofs/BussproofsItems.ts +++ b/ts/input/tex/bussproofs/BussproofsItems.ts @@ -96,7 +96,7 @@ export class ProofTreeItem extends BaseItem { * * @param {MmlNode} tree The proof tree. */ - private alignProof(tree: MmlNode) { + protected alignProof(tree: MmlNode) { const align = this.getProperty('proofAlign') as string; if (!align || align === 'normal') { return;