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.)
We now ensure that groups starting with `\*` never cause
text to be added to the document.
In addition, bookmarks now create a span between the start
and end of the bookmark, rather than an empty span.
