From 6535c031edc52fb7f145eea455fd481163b28a92 Mon Sep 17 00:00:00 2001
From: "Davide P. Cervone" <dpvc@union.edu>
Date: Sat, 3 Oct 2015 08:31:17 -0400
Subject: [PATCH] Fix alignment problems with horizontal stretched characters. 
 Resolves issue #1276.

---
 unpacked/jax/output/CommonHTML/jax.js | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/unpacked/jax/output/CommonHTML/jax.js b/unpacked/jax/output/CommonHTML/jax.js
index e8b8df0e1..980c532d4 100644
--- a/unpacked/jax/output/CommonHTML/jax.js
+++ b/unpacked/jax/output/CommonHTML/jax.js
@@ -1099,13 +1099,12 @@
         }
       }
       node.appendChild(right);
-      this.adjustHeights([left,ext,mid,ext2,right],hbox);
       if (ebox.D) ebox.d = ebox.D;
-      hbox.t = hbox.h; hbox.b = hbox.d;
-      var mt = ebox.h - hbox.h - ebox.a, mb = ebox.d - hbox.d + ebox.a;
+      hbox.t = hbox.h; hbox.b = hbox.d; hbox.h = ebox.h; hbox.d = ebox.d;
+      this.adjustHeights([left,ext,mid,ext2,right],hbox);
+      var mt = ebox.h - hbox.t - ebox.a, mb = ebox.d - hbox.b + ebox.a;
       if (mt) node.style.marginTop = CHTML.Em(mt);
       if (mb) node.style.marginBottom = CHTML.Em(mb);
-      hbox.h = ebox.h; hbox.d = ebox.d;
       if (BBOX) {hbox.scale = BBOX.scale; hbox.rscale = BBOX.rscale}
       return hbox;
     },
@@ -1114,10 +1113,12 @@
       //  To get alignment right in horizontal delimiters, we force all
       //  the elements to the same height and depth
       //
-      var T = CHTML.Em(bbox.h), D = CHTML.Em(bbox.d);
+      var T = CHTML.Em(bbox.t), D = CHTML.Em(bbox.b);
+      if (bbox.d < 0) {bbox.D = bbox.d; bbox.d = 0; D = CHTML.Em(-bbox.D+bbox.b)}
       for (var i = 0, m = nodes.length; i < m; i++) if (nodes[i]) {
         nodes[i].style.paddingTop = T;
         nodes[i].style.paddingBottom = D;
+        nodes[i].style.marginTop = nodes[i].style.marginBottom = 0;
       }
     },
     createChar: function (node,data,scale,font) {