Force width of -explicitFont text (work around Safari bug) #699
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR worked around a bug with WebKit that mis-measures regular text (like error messages) and so produces the wrong bounding boxes. For example, a TeX error message will get the yellow background size wrong. The problem is that the MJXZERO font seems to confuse WebKit (that is also the source of the problem with parts of characters disappearing). I'd like to fix this during the font update this summer, but for now, this is a work-around.
The fix is to remove the MJXZERO font during the measuring process, and then specify the width explicitly on the final text element. Not great, but it works for now.
You can test in Safari by causing any TeX error (e.g.,
\end
with no name, or\begin{xyz}
).