Remove use of css transforms for handling strechy assemblies in CHTML output

[dpvc]

This PR changes the way that CHTML output handles the extenders in stretchy characters. In the past, the extender was stretched using a CSS transform and clipped to the correct length via a CSS overflow setting on the mjx-ext element that contained it. This was fragile, and often lead to a displacement between the extender and its ends.

Here, we change to using multiple extender characters instead. We use a few more characters than actually needed, offset to make sure they overlap the ends, and retain the clipping to cut the extender to the right length or height. The old overflow settings are replaced by clip-region CSS, since using clip in overflow cause a separate rendering region which caused clipping in the other dimension, even when set to visible, leading to some unwanted clipping when the bounding box is very tight on the extender. The clip-region approach can be made to avoid that problem.

For horizontal extenders, the letter-spacing CSS can be used to reduce the gap between extenders when the character's width has non-zero left- or right-bearing values. To handle this, the font data for delimiters has a new property ext that records the size of the gap to be removed. That means you need to use new versions of the fonts that include this data. I will push new versions soon. Since those will use the scoped package names, you need to test this using a branch that also merges the woff2 branch, which switches to the scoped fonts.

For vertical extenders, we use white-space:pre and stack the extenders with \n in between, then adjust the line-height to get them to touch. Unfortunately, WebKit (so Safari) is not very accurate about its line-height handling, so I had to add extra extender characters to compensate, and even so, there can still be internal gaps. I was not able to come up with a mechanism that was guaranteed to work in Safari. Still, this produces better results over-all and all zoom levels than the transform approach.

In both cases, a new mjx-spacer element is used to adjust the position of the collection of extender characters within the mjx-ext element to ensure connections to the end pieces.

Some IE-specific CSS has been removed, as we are no longer able to support IE.

A border with of .1px rather than 0 is used in some CSS to avoid an alignment bug in Safari.

This also includes some of the change in the #1171, to properly clip the selection box for the stretchy assemblies.

[dpvc]

The new fonts are now in place.

[zorkow]

Couple of concerns in Wrappers/mo.ts. Please see my comments.

[dpvc]

I've made the changes, other than the * 0.5 vs / 2 as I think that should be done globally rather than piecemeal. I also didn't do anything about the null part[...] issue, as it is avoided as I explained in the comments above.

Can you re-review? Thanks.,

[zorkow]

lgtm.