www

commit 14fd3918eda0615fca0d18ec5a096733de188eb3
parent 13b16f9b26df1298110130bfa32dfeed2b07de26
Author: Davide P. Cervone <dpvc@union.edu>
Date:   Mon,  8 Sep 2014 15:23:42 -0400

Use delimitershortfall and delimiterfactor for stretching vertical delimiters.  Resolves issue #829.

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

1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/unpacked/jax/output/HTML-CSS/jax.js b/unpacked/jax/output/HTML-CSS/jax.js
@@ -1680,7 +1680,7 @@
       scriptspace:         .1,
       nulldelimiterspace:  .12,
       delimiterfactor:     901,
-      delimitershortfall:   .1,    // originally .3,
+      delimitershortfall:   .3,
 
       min_rule_thickness:  1.25     // in pixels
     },
@@ -2208,6 +2208,8 @@
 	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);
 	H = Math.max(values.minsize,Math.min(values.maxsize,H));
+        if (H != values.minsize)
+          {H = [Math.max(H*HTMLCSS.TeX.delimiterfactor/1000,H-HTMLCSS.TeX.delimitershortfall),H]}
 	span = this.HTMLcreateSpan(box); // clear contents and attributes
 	HTMLCSS.createDelimiter(span,this.data.join("").charCodeAt(0),H,scale);
 	if (values.symmetric) {H = (span.bbox.h + span.bbox.d)/2 + axis}