From 14fd3918eda0615fca0d18ec5a096733de188eb3 Mon Sep 17 00:00:00 2001 From: "Davide P. Cervone" Date: Mon, 8 Sep 2014 15:23:42 -0400 Subject: [PATCH 1/2] Use delimitershortfall and delimiterfactor for stretching vertical delimiters. Resolves issue #829. --- 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 index 7a5292568..0e325f26e 100644 --- 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} From 177eade96426bf980777221bf02e9265d2001133 Mon Sep 17 00:00:00 2001 From: "Davide P. Cervone" Date: Mon, 8 Sep 2014 15:27:31 -0400 Subject: [PATCH 2/2] Use delimitershortfall and delimiterfactor for stretching vertical delimiters for SVG. --- 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 index 33a01ea9c..858846578 100644 --- 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)}