www

commit 177eade96426bf980777221bf02e9265d2001133
parent 14fd3918eda0615fca0d18ec5a096733de188eb3
Author: Davide P. Cervone <dpvc@union.edu>
Date:   Mon,  8 Sep 2014 15:27:31 -0400

Use delimitershortfall and delimiterfactor for stretching vertical delimiters for SVG.

Diffstat:
M
unpacked/jax/output/SVG/jax.js
 | 
4
+++-

1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/unpacked/jax/output/SVG/jax.js b/unpacked/jax/output/SVG/jax.js
@@ -814,7 +814,7 @@
       scriptspace:         100,
       nulldelimiterspace:  120,
       delimiterfactor:     901,
-      delimitershortfall:  100,    // originally 300,
+      delimitershortfall:  300,
 
       min_rule_thickness:  1.25,   // in pixels
       min_root_space:      1.5     // in pixels
@@ -1488,6 +1488,8 @@
 	values.maxsize = SVG.length2em(values.maxsize,mu,svg.h+svg.d);
 	values.minsize = SVG.length2em(values.minsize,mu,svg.h+svg.d);
 	H = Math.max(values.minsize,Math.min(values.maxsize,H));
+        if (H != values.minsize)
+          {H = [Math.max(H*SVG.TeX.delimiterfactor/1000,H-SVG.TeX.delimitershortfall),H]}
 	svg = SVG.createDelimiter(this.data.join("").charCodeAt(0),H,svg.scale);
 	if (values.symmetric) {H = (svg.h + svg.d)/2 + axis}
 	  else {H = (svg.h + svg.d) * h/(h + d)}