search

metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
25 stars 9 forks source link

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

Closed digama0 closed 1 year ago

digama0 commented 2 years ago

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 commented 1 year ago

(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 commented 1 year ago

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 commented 1 year ago

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

jkingdon commented 1 year ago

@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.