add double-quote escape in $t/$j comments

[digama0]

This adds support for strings like "ab""c" in $t and $j comments which encode the string ab"c.

Some additional care is required in user code, since now the body of a string is no longer the actual contents of the string but rather doubled characters have to be unescaped. We return a Cow now and check for the very common case of no escapes to avoid the copy most of the time. But if working directly with string spans, CommandToken::unescape_string should be used to get the value now.

[tirix]

(Coming back to this after a long break!)
The logic of this PR is good, even if I don't see a current use-case.

My only issue would be with the changes in grammar.rs, which seem to be unrelated, and conflicting with other changes in main.
Could you revert the changes in grammar.rs / move them to a different PR?

[jkingdon]

It would appear this correctly handles the following cases from the Metamath Book (section 4.4.2), which has a fair amount of detail about what the rules are supposed to be:

Example	Meaning
"a""b"	a"b
’c’’d’	c’d
"e’’f"	e’’f
’g""h’	g""h

[tirix]

@jkingdon @digama0 shouldn't we merge this PR? What is blocking here?

[jkingdon]

@jkingdon @digama0 shouldn't we merge this PR? What is blocking here?

Not sure I looked carefully enough (either by code inspection, or by writing unit tests) to provide too much input, but I don't object.