(span, options, style)
| 8134 | }; |
| 8135 | |
| 8136 | var centerSpan = function centerSpan(span, options, style) { |
| 8137 | var newOptions = options.havingBaseStyle(style); |
| 8138 | var shift = (1 - options.sizeMultiplier / newOptions.sizeMultiplier) * options.fontMetrics().axisHeight; |
| 8139 | span.classes.push("delimcenter"); |
| 8140 | span.style.top = shift + "em"; |
| 8141 | span.height -= shift; |
| 8142 | span.depth += shift; |
| 8143 | }; |
| 8144 | /** |
| 8145 | * Makes a small delimiter. This is a delimiter that comes in the Main-Regular |
| 8146 | * font, but is restyled to either be in textstyle, scriptstyle, or |
no test coverage detected