From c54ac491086e65a0c8bc4219bc54ef3867d1dcf5 Mon Sep 17 00:00:00 2001
From: "Davide P. Cervone" <dpvc@union.edu>
Date: Wed, 8 Jan 2014 11:44:23 -0500
Subject: [PATCH] Scale axis sizes properly for scripts.  Issue #703.

---
 unpacked/jax/output/HTML-CSS/jax.js | 2 +-
 unpacked/jax/output/SVG/jax.js      | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/unpacked/jax/output/HTML-CSS/jax.js b/unpacked/jax/output/HTML-CSS/jax.js
index 6ece947af..2405c5d78 100644
--- a/unpacked/jax/output/HTML-CSS/jax.js
+++ b/unpacked/jax/output/HTML-CSS/jax.js
@@ -2121,7 +2121,7 @@
 	this.HTMLremoveColor();
 	var values = this.getValues("symmetric","maxsize","minsize");
 	var span = this.HTMLspanElement(), mu = this.HTMLgetMu(span), H;
-	var axis = HTMLCSS.TeX.axis_height, scale = span.scale;
+	var scale = span.scale, axis = HTMLCSS.TeX.axis_height * scale;
 	if (values.symmetric) {H = 2*Math.max(h-axis,d+axis)} else {H = h + d}
 	values.maxsize = HTMLCSS.length2em(values.maxsize,mu,span.bbox.h+span.bbox.d);
 	values.minsize = HTMLCSS.length2em(values.minsize,mu,span.bbox.h+span.bbox.d);
diff --git a/unpacked/jax/output/SVG/jax.js b/unpacked/jax/output/SVG/jax.js
index 7a44aeee0..903859c8f 100644
--- a/unpacked/jax/output/SVG/jax.js
+++ b/unpacked/jax/output/SVG/jax.js
@@ -1327,7 +1327,7 @@
         //
         //  Get the variant, and check for operator size
         //
-        var scale = this.SVGgetScale(), variant = this.SVGgetVariant();
+        var scale = svg.scale = this.SVGgetScale(), variant = this.SVGgetVariant();
 	var values = this.getValues("largeop","displaystyle");
 	if (values.largeop)
 	  {variant = SVG.FONTDATA.VARIANT[values.displaystyle ? "-largeOp" : "-smallOp"]}
@@ -1425,7 +1425,7 @@
       SVGstretchV: function (h,d) {
         var svg = this.svg || this.toSVG();
 	var values = this.getValues("symmetric","maxsize","minsize");
-	var axis = SVG.TeX.axis_height, mu = this.SVGgetMu(svg), H;
+	var axis = SVG.TeX.axis_height*svg.scale, mu = this.SVGgetMu(svg), H;
 	if (values.symmetric) {H = 2*Math.max(h-axis,d+axis)} else {H = h + d}
 	values.maxsize = SVG.length2em(values.maxsize,mu,svg.h+svg.d);
 	values.minsize = SVG.length2em(values.minsize,mu,svg.h+svg.d);
@@ -1496,7 +1496,7 @@
 	var values = this.getValues("height","depth","width");
 	values.mathbackground = this.mathbackground;
 	if (this.background && !this.mathbackground) {values.mathbackground = this.background}
-        var svg = this.SVG(), mu = this.SVGgetMu(svg);
+        var svg = this.SVG(), mu = this.SVGgetMu(svg); 
 	svg.h = SVG.length2em(values.height,mu) / svg.scale;
         svg.d = SVG.length2em(values.depth,mu)  / svg.scale;
 	svg.w = svg.r = SVG.length2em(values.width,mu) / svg.scale;