From 397dcb303baa8285968ba5ce5038d052259b726e Mon Sep 17 00:00:00 2001
From: Martin von Gagern <gagern@ma.tum.de>
Date: Sat, 13 Jun 2015 21:14:35 +0200
Subject: [PATCH] Simplify stacked delimiters

Using a loop to determine the number of symbols we need is intuitive but
hardly efficient.  A Math.ceil in this situation is much better.

After that ceil or the loop that it replaced, the total height should be
equal to the minimal height plus an integral number times the height of the
repeat symbol.  That integer equals (half) number of loop iterations in the
original code, and the repeatCount variable in my new code.  So later on,
the quotient (repeatHeight / repeatHeightTotal) should be an integer, at
least up to numeric errors.  Applying ceil instead of round to that is
asking for these numeric errors to seriously break stuff.  Just reusing the
repeatCount is much simpler, shorter and more elegant.

Having distinct topSymbolCount and bottomSymbolCount seems pointless, since
the only reason why these could ever be different is due to the fact that
bottomRepeatHeight was computed using topHeightTotal, which looks like a
bug.  The old loop and new ceil assume a symmetric repeatCount.
---
 src/delimiter.js | 58 ++++++++++++++----------------------------------
 1 file changed, 17 insertions(+), 41 deletions(-)

diff --git a/src/delimiter.js b/src/delimiter.js
index a0e7f0c9b..91e52f212 100644
--- a/src/delimiter.js
+++ b/src/delimiter.js
@@ -231,28 +231,25 @@ var makeStackedDelim = function(delim, heightTotal, center, options, mode) {
     var repeatHeightTotal = repeatMetrics.height + repeatMetrics.depth;
     var bottomMetrics = getMetrics(bottom, font);
     var bottomHeightTotal = bottomMetrics.height + bottomMetrics.depth;
-    var middleMetrics, middleHeightTotal;
+    var middleHeightTotal = 0;
+    var middleFactor = 1;
     if (middle !== null) {
-        middleMetrics = getMetrics(middle, font);
+        var middleMetrics = getMetrics(middle, font);
         middleHeightTotal = middleMetrics.height + middleMetrics.depth;
+        middleFactor = 2; // repeat symmetrically above and below middle
     }
 
-    // Calcuate the real height that the delimiter will have. It is at least the
-    // size of the top, bottom, and optional middle combined.
-    var realHeightTotal = topHeightTotal + bottomHeightTotal;
-    if (middle !== null) {
-        realHeightTotal += middleHeightTotal;
-    }
+    // Calcuate the minimal height that the delimiter can have.
+    // It is at least the size of the top, bottom, and optional middle combined.
+    var minHeight = topHeightTotal + bottomHeightTotal + middleHeightTotal;
 
-    // Then add repeated pieces until we reach the specified height.
-    while (realHeightTotal < heightTotal) {
-        realHeightTotal += repeatHeightTotal;
-        if (middle !== null) {
-            // If there is a middle section, we need an equal number of pieces
-            // on the top and bottom.
-            realHeightTotal += repeatHeightTotal;
-        }
-    }
+    // Compute the number of copies of the repeat symbol we will need
+    var repeatCount = Math.ceil(
+        (heightTotal - minHeight) / (middleFactor * repeatHeightTotal));
+
+    // Compute the total height of the delimiter including all the symbols
+    var realHeightTotal =
+        minHeight + repeatCount * middleFactor * repeatHeightTotal;
 
     // The center of the delimiter is placed at the center of the axis. Note
     // that in this context, "center" means that the delimiter should be
@@ -275,39 +272,18 @@ var makeStackedDelim = function(delim, heightTotal, center, options, mode) {
 
     var i;
     if (middle === null) {
-        // Calculate the number of repeated symbols we need
-        var repeatHeight = realHeightTotal - topHeightTotal - bottomHeightTotal;
-        var symbolCount = Math.ceil(repeatHeight / repeatHeightTotal);
-
         // Add that many symbols
-        for (i = 0; i < symbolCount; i++) {
+        for (i = 0; i < repeatCount; i++) {
             inners.push(makeInner(repeat, font, mode));
         }
     } else {
         // When there is a middle bit, we need the middle part and two repeated
         // sections
-
-        // Calculate the number of symbols needed for the top and bottom
-        // repeated parts
-        var topRepeatHeight =
-            realHeightTotal / 2 - topHeightTotal - middleHeightTotal / 2;
-        var topSymbolCount = Math.ceil(topRepeatHeight / repeatHeightTotal);
-
-        var bottomRepeatHeight =
-            realHeightTotal / 2 - topHeightTotal - middleHeightTotal / 2;
-        var bottomSymbolCount =
-            Math.ceil(bottomRepeatHeight / repeatHeightTotal);
-
-        // Add the top repeated part
-        for (i = 0; i < topSymbolCount; i++) {
+        for (i = 0; i < repeatCount; i++) {
             inners.push(makeInner(repeat, font, mode));
         }
-
-        // Add the middle piece
         inners.push(makeInner(middle, font, mode));
-
-        // Add the bottom repeated part
-        for (i = 0; i < bottomSymbolCount; i++) {
+        for (i = 0; i < repeatCount; i++) {
             inners.push(makeInner(repeat, font, mode));
         }
     }