(span, options, style)
| 8006 | }; |
| 8007 | |
| 8008 | const centerSpan = function centerSpan(span, options, style) { |
| 8009 | const newOptions = options.havingBaseStyle(style); |
| 8010 | const shift = (1 - options.sizeMultiplier / newOptions.sizeMultiplier) * options.fontMetrics().axisHeight; |
| 8011 | span.classes.push("delimcenter"); |
| 8012 | span.style.top = shift + "em"; |
| 8013 | span.height -= shift; |
| 8014 | span.depth += shift; |
| 8015 | }; |
| 8016 | /** |
| 8017 | * Makes a small delimiter. This is a delimiter that comes in the Main-Regular |
| 8018 | * font, but is restyled to either be in textstyle, scriptstyle, or |
no test coverage detected