From 49003fe4ac1b9bbb1196abef82b685cdf08acf8e Mon Sep 17 00:00:00 2001 From: "Davide P. Cervone" Date: Thu, 3 Dec 2015 11:49:55 -0500 Subject: [PATCH 1/2] Fix vertical stretchy characters to use multiple extenders rather than CSS transform. Issue #1326 --- unpacked/jax/output/CommonHTML/jax.js | 41 ++++++++++++++------------- 1 file changed, 21 insertions(+), 20 deletions(-) diff --git a/unpacked/jax/output/CommonHTML/jax.js b/unpacked/jax/output/CommonHTML/jax.js index f664b7941..fa037ed04 100644 --- a/unpacked/jax/output/CommonHTML/jax.js +++ b/unpacked/jax/output/CommonHTML/jax.js @@ -34,6 +34,7 @@ var EVENT, TOUCH, HOVER; // filled in later var STRUTHEIGHT = 1, + EFUZZ = .1, // overlap needed for stretchy delimiters HFUZZ = .025, DFUZZ = .025; // adjustments to bounding box of character boxes var STYLES = { @@ -665,6 +666,9 @@ pxPerInch: 96, em: 16, + maxStretchyParts: 1000, // limit the number of parts allowed for + // stretchy operators. See issue 366. + FONTDEF: {}, TEXDEF: { x_height: .442, @@ -1009,11 +1013,11 @@ }, extendDelimiterV: function (node,H,delim,BBOX,font) { node = CHTML.addElement(node,"mjx-delim-v"); var tmp = CHTML.Element("span"); - var top, bot, mid, ext, tbox, bbox, mbox, ebox, k = 1; + var top, bot, mid, ext, tbox, bbox, mbox, ebox, k = 1, c; tbox = this.createChar(tmp,(delim.top||delim.ext),1,font); top = tmp.removeChild(tmp.firstChild); bbox = this.createChar(tmp,(delim.bot||delim.ext),1,font); bot = tmp.removeChild(tmp.firstChild); mbox = ebox = CHTML.BBOX.zero(); - var h = tbox.h + tbox.d + bbox.h + bbox.d; + var h = tbox.h + tbox.d + bbox.h + bbox.d - EFUZZ; node.appendChild(top); if (delim.mid) { mbox = this.createChar(tmp,delim.mid,1,font); mid = tmp.removeChild(tmp.firstChild); @@ -1022,30 +1026,27 @@ if (delim.min && H < h*delim.min) H = h*delim.min; if (H > h) { ebox = this.createChar(tmp,delim.ext,1,font); ext = tmp.removeChild(tmp.firstChild); - if (delim.fullExtenders) { - var n = Math.ceil((H-h)/(k*(ebox.h+ebox.d)*.9)); - H = .9*n*k*(ebox.h+ebox.d) + h; - } - var s = 1.1*(H - h)/k + .3; // space to cover by extender - s /= (ebox.h+ebox.d); // scale factor; - this.Transform(ext, - "translateY("+CHTML.Em(-ebox.d+.25-s*ebox.a)+") scaleY("+s.toFixed(3).replace(/0+$/,"")+")", - "left "+CHTML.Em(ebox.d) - ); - ext.style.paddingTop=ext.style.paddingBottom = 0; - top.style.marginBottom = CHTML.Em((H-h)/k); + var eH = ebox.h + ebox.d, eh = eH - EFUZZ, n, N; + N = n = Math.min(Math.ceil((H-h)/(k*eh)),this.maxStretchyParts); + if (delim.fullExtenders) H = n*k*eh + h; else eh = (H-h)/(k*n); + c = ebox.d+ebox.a-eH/2; // for centering of extenders + ext.style.margin = ext.style.padding = ""; + ext.style.lineHeight = CHTML.Em(eh); + ext.style.marginBottom = CHTML.Em(c-EFUZZ/2/k); + ext.style.marginTop = CHTML.Em(-c-EFUZZ/2/k); + var TEXT = ext.textContent, text = "\n"+TEXT; + while (--n > 0) TEXT += text; + ext.firstChild.textContent = TEXT; node.appendChild(ext); if (delim.mid) { node.appendChild(mid); - mid.style.marginBottom = top.style.marginBottom; node.appendChild(ext.cloneNode(true)); } } else { - H = h - .25; top.style.marginBottom = "-.25em"; - if (delim.mid) { - node.appendChild(mid); - mid.style.marginBottom = "-.3em"; H -= .1; - } + c = (H-h-EFUZZ) / k; + top.style.marginBottom = CHTML.Em(c+parseFloat(top.style.marginBottom||"0")); + if (delim.mid) node.appendChild(mid); + bot.style.marginTop = CHTML.Em(c+parseFloat(bot.style.marginTop||"0")); } node.appendChild(bot); var vbox = CHTML.BBOX({ From 206dc7f4903f415f9861ee067f81146f543a2a1c Mon Sep 17 00:00:00 2001 From: "Davide P. Cervone" Date: Fri, 4 Dec 2015 10:28:54 -0500 Subject: [PATCH 2/2] Make horizontal stretchy characters use multiple extenders rather than CSS transform. Issue #1326 --- unpacked/jax/output/CommonHTML/jax.js | 73 ++++++++++++--------------- 1 file changed, 33 insertions(+), 40 deletions(-) diff --git a/unpacked/jax/output/CommonHTML/jax.js b/unpacked/jax/output/CommonHTML/jax.js index fa037ed04..f8b438d38 100644 --- a/unpacked/jax/output/CommonHTML/jax.js +++ b/unpacked/jax/output/CommonHTML/jax.js @@ -96,12 +96,7 @@ ".mjx-prestack > .mjx-presup": {display:"block"}, ".mjx-prestack > .mjx-presub": {display:"block"}, - ".mjx-delim-v > .mjx-char": {transform:"scale(1)"}, // for Firefox to get horizontal alignment better - ".mjx-delim-h": {display:"block"}, - ".mjx-delim-h > .mjx-char": { - transform:"scale(1)", - display:"inline-block" - }, + ".mjx-delim-h > .mjx-char": {display:"inline-block"}, ".mjx-surd": {"vertical-align":"top"}, @@ -1026,10 +1021,10 @@ if (delim.min && H < h*delim.min) H = h*delim.min; if (H > h) { ebox = this.createChar(tmp,delim.ext,1,font); ext = tmp.removeChild(tmp.firstChild); - var eH = ebox.h + ebox.d, eh = eH - EFUZZ, n, N; - N = n = Math.min(Math.ceil((H-h)/(k*eh)),this.maxStretchyParts); + var eH = ebox.h + ebox.d, eh = eH - EFUZZ; + var n = Math.min(Math.ceil((H-h)/(k*eh)),this.maxStretchyParts); if (delim.fullExtenders) H = n*k*eh + h; else eh = (H-h)/(k*n); - c = ebox.d+ebox.a-eH/2; // for centering of extenders + c = ebox.d + ebox.a - eH/2; // for centering of extenders ext.style.margin = ext.style.padding = ""; ext.style.lineHeight = CHTML.Em(eh); ext.style.marginBottom = CHTML.Em(c-EFUZZ/2/k); @@ -1065,64 +1060,62 @@ lbox = this.createChar(tmp,(delim.left||delim.rep),1,font); left = tmp.removeChild(tmp.firstChild); rbox = this.createChar(tmp,(delim.right||delim.rep),1,font); right = tmp.removeChild(tmp.firstChild); ebox = this.createChar(tmp,delim.rep,1,font); ext = tmp.removeChild(tmp.firstChild); + left.style.marginLeft = CHTML.Em(-lbox.l); + right.style.marginRight = CHTML.Em(rbox.r-rbox.w); node.appendChild(left); var hbox = CHTML.BBOX.zero(); - hbox.h = Math.max(lbox.h,rbox.h); hbox.d = Math.max(lbox.d,rbox.d); - left.style.marginLeft = CHTML.Em(-lbox.l); left.style.marginRight = CHTML.Em(lbox.r-lbox.w); - right.style.marginleft = CHTML.Em(-rbox.l); right.style.marginRight = CHTML.Em(rbox.r-rbox.w); - var w = (lbox.r - lbox.l) + (rbox.r - rbox.l) - .05; + hbox.h = Math.max(lbox.h,rbox.h,ebox.h); + hbox.d = Math.max(lbox.D||lbox.d,rbox.D||rbox.d,ebox.D||ebox.d); + var w = (lbox.r - lbox.l) + (rbox.r - rbox.l) - EFUZZ; if (delim.mid) { mbox = this.createChar(tmp,delim.mid,1,font); mid = tmp.removeChild(tmp.firstChild); - w += mbox.w; k = 2; + mid.style.marginleft = CHTML.Em(-mbox.l); mid.style.marginRight = CHTML.Em(mbox.r-mbox.w); + w += mbox.r - mbox.l + EFUZZ; k = 2; if (mbox.h > hbox.h) hbox.h = mbox.h; if (mbox.d > hbox.d) hbox.d = mbox.d; } if (delim.min && W < w*delim.min) W = w*delim.min; - right.style.marginLeft = CHTML.Em((W-w-rbox.l)/k); hbox.w = hbox.r = W; if (W > w) { - if (ebox.h > hbox.h) hbox.h = ebox.h; - if (ebox.d > hbox.d) hbox.d = ebox.d; - var s = (W - w)/k + .2; // space to cover by extender - s /= (ebox.r - ebox.l); // scale factor - this.Transform(ext, - "translateX("+CHTML.Em(-ebox.l-.1)+") scaleX("+s.toFixed(3).replace(/0+$/,"")+")", - CHTML.Em(ebox.l)+" center" - ); - ext.style.width = 0; + var eW = ebox.r-ebox.l, ew = eW - EFUZZ; + var n = Math.min(Math.ceil((W-w)/(k*ew)),this.maxStretchyParts); + if (delim.fullExtenders) W = n*k*ew + w; else ew = (W-w)/(k*n); + var c = (eW - ew + EFUZZ/k) / 2; // for centering of extenders + ext.style.marginLeft = CHTML.Em(-ebox.l-c); + ext.style.marginRight = CHTML.Em(ebox.r-ebox.w+c); + ext.style.letterSpacing = CHTML.Em(-(ebox.w-ew)); + left.style.marginRight = CHTML.Em(lbox.r-lbox.w); + right.style.marginleft = CHTML.Em(-rbox.l); + var TEXT = ext.textContent, text = TEXT; + while (--n > 0) TEXT += text; + ext.firstChild.textContent = TEXT; node.appendChild(ext); if (delim.mid) { node.appendChild(mid); - mid.style.marginLeft = right.style.marginLeft; ext2 = node.appendChild(ext.cloneNode(true)); } } else { - if (delim.mid) { - node.appendChild(mid); - mid.style.marginLeft = CHTML.Em((W-w)/k); - } + c = (W-w-EFUZZ/k) / 2; + left.style.marginRight = CHTML.Em(lbox.r-lbox.w+c); + if (delim.mid) node.appendChild(mid); + right.style.marginLeft = CHTML.Em(-rbox.l+c); } node.appendChild(right); - if (ebox.D) ebox.d = ebox.D; - 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); + this.adjustHeights([left,ext,mid,ext2,right],[lbox,ebox,mbox,ebox,rbox],hbox); if (BBOX) {hbox.scale = BBOX.scale; hbox.rscale = BBOX.rscale} return hbox; }, - adjustHeights: function (nodes,bbox) { + adjustHeights: function (nodes,box,bbox) { // // To get alignment right in horizontal delimiters, we force all // the elements to the same height and depth // - 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)} + var T = bbox.h, B = bbox.d; + if (bbox.d < 0) {B = -bbox.d; bbox.D = bbox.d; bbox.d = 0} 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.paddingTop = CHTML.Em(T-box[i].a); + nodes[i].style.paddingBottom = CHTML.Em(B+box[i].a); nodes[i].style.marginTop = nodes[i].style.marginBottom = 0; } },