Prevent gaps in tall delimiters (#1986)
* Prevent gaps in tall delimiters * Improve lap vertical alignment * Fix lint errors * Remove outdated comment * Move a declaration out of makeStackedDelim() * Update screenshots
@@ -178,6 +178,9 @@ const makeInner = function(
|
|||||||
return {type: "elem", elem: inner};
|
return {type: "elem", elem: inner};
|
||||||
};
|
};
|
||||||
|
|
||||||
|
// Helper for makeStackedDelim
|
||||||
|
const lap = {type: "kern", size: -0.005};
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Make a stacked delimiter out of a given delimiter, with the total height at
|
* Make a stacked delimiter out of a given delimiter, with the total height at
|
||||||
* least `heightTotal`. This routine is mentioned on page 442 of the TeXbook.
|
* least `heightTotal`. This routine is mentioned on page 442 of the TeXbook.
|
||||||
@@ -310,8 +313,8 @@ const makeStackedDelim = function(
|
|||||||
const minHeight = topHeightTotal + bottomHeightTotal + middleHeightTotal;
|
const minHeight = topHeightTotal + bottomHeightTotal + middleHeightTotal;
|
||||||
|
|
||||||
// Compute the number of copies of the repeat symbol we will need
|
// Compute the number of copies of the repeat symbol we will need
|
||||||
const repeatCount = Math.ceil(
|
const repeatCount = Math.max(0, Math.ceil(
|
||||||
(heightTotal - minHeight) / (middleFactor * repeatHeightTotal));
|
(heightTotal - minHeight) / (middleFactor * repeatHeightTotal)));
|
||||||
|
|
||||||
// Compute the total height of the delimiter including all the symbols
|
// Compute the total height of the delimiter including all the symbols
|
||||||
const realHeightTotal =
|
const realHeightTotal =
|
||||||
@@ -328,6 +331,15 @@ const makeStackedDelim = function(
|
|||||||
// Calculate the depth
|
// Calculate the depth
|
||||||
const depth = realHeightTotal / 2 - axisHeight;
|
const depth = realHeightTotal / 2 - axisHeight;
|
||||||
|
|
||||||
|
// This function differs from the TeX procedure in one way.
|
||||||
|
// We shift each repeat element downwards by 0.005em, to prevent a gap
|
||||||
|
// due to browser floating point rounding error.
|
||||||
|
// Then, at the last element-to element joint, we add one extra repeat
|
||||||
|
// element to cover the gap created by the shifts.
|
||||||
|
// Find the shift needed to align the upper end of the extra element at a point
|
||||||
|
// 0.005em above the lower end of the top element.
|
||||||
|
const shiftOfExtraElement = (repeatCount + 1) * 0.005 - repeatHeightTotal;
|
||||||
|
|
||||||
// Now, we start building the pieces that will go into the vlist
|
// Now, we start building the pieces that will go into the vlist
|
||||||
|
|
||||||
// Keep a list of the inner pieces
|
// Keep a list of the inner pieces
|
||||||
@@ -339,20 +351,34 @@ const makeStackedDelim = function(
|
|||||||
if (middle === null) {
|
if (middle === null) {
|
||||||
// Add that many symbols
|
// Add that many symbols
|
||||||
for (let i = 0; i < repeatCount; i++) {
|
for (let i = 0; i < repeatCount; i++) {
|
||||||
|
inners.push(lap); // overlap
|
||||||
inners.push(makeInner(repeat, font, mode));
|
inners.push(makeInner(repeat, font, mode));
|
||||||
}
|
}
|
||||||
} else {
|
} else {
|
||||||
// When there is a middle bit, we need the middle part and two repeated
|
// When there is a middle bit, we need the middle part and two repeated
|
||||||
// sections
|
// sections
|
||||||
for (let i = 0; i < repeatCount; i++) {
|
for (let i = 0; i < repeatCount; i++) {
|
||||||
|
inners.push(lap);
|
||||||
inners.push(makeInner(repeat, font, mode));
|
inners.push(makeInner(repeat, font, mode));
|
||||||
}
|
}
|
||||||
|
// Insert one extra repeat element.
|
||||||
|
inners.push({type: "kern", size: shiftOfExtraElement});
|
||||||
|
inners.push(makeInner(repeat, font, mode));
|
||||||
|
inners.push(lap);
|
||||||
|
// Now insert the middle of the brace.
|
||||||
inners.push(makeInner(middle, font, mode));
|
inners.push(makeInner(middle, font, mode));
|
||||||
for (let i = 0; i < repeatCount; i++) {
|
for (let i = 0; i < repeatCount; i++) {
|
||||||
|
inners.push(lap);
|
||||||
inners.push(makeInner(repeat, font, mode));
|
inners.push(makeInner(repeat, font, mode));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// To cover the gap create by the overlaps, insert one more repeat element,
|
||||||
|
// at a position that juts 0.005 above the bottom of the top element.
|
||||||
|
inners.push({type: "kern", size: shiftOfExtraElement});
|
||||||
|
inners.push(makeInner(repeat, font, mode));
|
||||||
|
inners.push(lap);
|
||||||
|
|
||||||
// Add the top symbol
|
// Add the top symbol
|
||||||
inners.push(makeInner(top, font, mode));
|
inners.push(makeInner(top, font, mode));
|
||||||
|
|
||||||
|
Before Width: | Height: | Size: 24 KiB After Width: | Height: | Size: 24 KiB |
Before Width: | Height: | Size: 23 KiB After Width: | Height: | Size: 23 KiB |
Before Width: | Height: | Size: 19 KiB After Width: | Height: | Size: 19 KiB |
Before Width: | Height: | Size: 18 KiB After Width: | Height: | Size: 18 KiB |
Before Width: | Height: | Size: 13 KiB After Width: | Height: | Size: 13 KiB |
Before Width: | Height: | Size: 11 KiB After Width: | Height: | Size: 11 KiB |
Before Width: | Height: | Size: 7.5 KiB After Width: | Height: | Size: 7.5 KiB |
Before Width: | Height: | Size: 7.5 KiB After Width: | Height: | Size: 7.6 KiB |
Before Width: | Height: | Size: 22 KiB After Width: | Height: | Size: 22 KiB |
Before Width: | Height: | Size: 19 KiB After Width: | Height: | Size: 19 KiB |
Before Width: | Height: | Size: 52 KiB After Width: | Height: | Size: 52 KiB |
Before Width: | Height: | Size: 43 KiB After Width: | Height: | Size: 43 KiB |
Before Width: | Height: | Size: 65 KiB After Width: | Height: | Size: 65 KiB |
Before Width: | Height: | Size: 54 KiB After Width: | Height: | Size: 54 KiB |
Before Width: | Height: | Size: 9.7 KiB After Width: | Height: | Size: 9.8 KiB |
Before Width: | Height: | Size: 7.1 KiB After Width: | Height: | Size: 7.1 KiB |