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

Statements parse error #79

Closed tirix closed 2 years ago

tirix commented 2 years ago

This splits off a special error type for statement parsing, and adds a new API for parsing a given string.

There are use cases where we want to parse a string outside of the database. In that case, the string exists by itself and it does not make sense to reference to a containing database statement when building the error messages.

This PR moves diagnostics specific to this use case to a different class of errors.

(Ideally we could still include spans when reporting errors, but these would be relative to the beginning of the string rather than a database segment - that part could be in a follow-up PR)

This PR also introduces a utility undefined_cmd to generate the Diagnostic::UndefinedToken error.