metamath / metamath-knife

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

Swap Notation for annotate_snippets::snippet::Snippet #49

Closed tirix closed 2 years ago

tirix commented 2 years ago

This is an attempt at using annotate_snippets::snippet::Snippet for the API, however I'm having issues with ownership ~and lifetime~ of the strings returned in the Snippet structures, so this is still WIP.

digama0 commented 2 years ago

What's the reason for using strfmt? Couldn't Diagnostic have a Display instance instead, that does e.g.

    match *diag {
        BadCharacter(span, byte) => {
            write!(f, "Invalid character (byte value {byte}); Metamath source files are limited to \
                      US-ASCII with controls TAB, CR, LF, FF)", byte = byte)?
        }
tirix commented 2 years ago

Thank you Mario!

tirix commented 2 years ago

This addresses one of the items of API issues #35.