From 177eade96426bf980777221bf02e9265d2001133 Mon Sep 17 00:00:00 2001 From: "Davide P. Cervone" Date: Mon, 8 Sep 2014 15:27:31 -0400 Subject: [PATCH] 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)}