commit 668585f5912f500a68f752e8260c854bde9c5d51
parent 8eb029478e6fb94976dc05959f54ecee7d0583cb
Author: Davide P. Cervone <dpvc@union.edu>
Date: Fri, 30 May 2014 12:17:09 -0400
Fix several problems with stretchy delimiters in SVG output (minsize didn't always get processed, stretched characters weren't marked as such).
Diffstat:
1 file changed, 12 insertions(+), 3 deletions(-)
diff --git a/unpacked/jax/output/SVG/jax.js b/unpacked/jax/output/SVG/jax.js
@@ -1325,8 +1325,15 @@
},
SVGcanStretch: function (direction) {
- if (this.isEmbellished()) {return this.Core().SVGcanStretch(direction)}
- return false;
+ var can = false;
+ if (this.isEmbellished()) {
+ var core = this.Core();
+ if (core && core !== this) {
+ can = core.SVGcanStretch(direction);
+ if (can && core.forceStretch) {this.forceStretch = true}
+ }
+ }
+ return can;
},
SVGstretchV: function (h,d) {return this.toSVG(h,d)},
SVGstretchH: function (w) {return this.toSVG(w)},
@@ -1425,7 +1432,7 @@
CoreParent: function () {
var parent = this;
while (parent && parent.isEmbellished() &&
- parent.CoreMO() === this && !parent.isa(MML.math)) {parent = parent.Parent()}
+ parent.CoreMO() === this && !parent.isa(MML.math)) {parent = parent.Parent()}
return parent;
},
CoreText: function (parent) {
@@ -1486,6 +1493,7 @@
this.SVGhandleColor(svg);
delete this.svg.element;
this.SVGsaveData(svg);
+ svg.stretched = true;
return svg;
},
SVGstretchH: function (w) {
@@ -1502,6 +1510,7 @@
this.SVGhandleColor(svg);
delete this.svg.element;
this.SVGsaveData(svg);
+ svg.stretched = true;
return svg;
}
});