Previously we used our own homespun formatting. But this
produces over-long lines that aren't ideal for diffs in tests.
Easier to use something off-the-shelf and standard.
Closes#7580.
Performance is slower by about a factor of 10, but this isn't
really a problem because native isn't suitable as a serialization
format. (For serialization you should use json, because the reader
is so much faster than native.)
Generally we allow optional starred variants of LaTeX commands
(since many allow them, and if we don't accept these explicitly,
ignoring the star usually gives acceptable results). But we
don't want to do this for `\(*\)` and similar cases.
Closes#7340.
