Better error handling in grammar #78
Conversation
src/diag.rs
Outdated
| "This token was not declared in any $v or $c statement".into(), | ||
| stmt, | ||
| *span, | ||
| )]), |
There was a problem hiding this comment.
Why is this not just UnknownToken? It should be an error condition (even though you won't get it unless you try to parse the grammar).
There was a problem hiding this comment.
UnknownToken already exists with a TokenIndex as parameter, while this version of the diagnostic has a Span.
UnknownCommandToken is currently only used within the commands, because we have no token index there, but just a span. I'm not sure if it might be used elsewhere.
Do you have a better naming (which does not collide with UnknownToken)?
There was a problem hiding this comment.
I feel like something similar would have come up in typesetting comment parsing... EDIT: I'm thinking of UndefinedToken, which comes with a span and the literal token text. The error is used in verify_markup.rs when checking typesetting comments.
There was a problem hiding this comment.
Sounds good, I think I can refactor to use UndefinedToken instead.
Note/Edit: UndefinedToken is a warning, anyway for $j comments I think maybe warning is actually better suited, since the database and proofs are actually correct.
src/grammar.rs
Outdated
| @@ -859,8 +866,9 @@ impl Grammar { | |||
| stype, | |||
| &next_node.with_reduce_vec(reduce_vec), | |||
| ) | |||
| .expect("Double conflict!"); | |||
| .map_err(|_| Diagnostic::GrammarCantBuild)?; // Double conflict | |||
There was a problem hiding this comment.
| .map_err(|_| Diagnostic::GrammarCantBuild)?; // Double conflict | |
| .map_err(|_| Diagnostic::GrammarCantBuild("Double conflict"))?; |
It's a shame to lose these comments in the output. If it stores a &'static str or Cow<'static, str> then you don't have to go to the trouble of creating an enum for these messages but you can still display them
There was a problem hiding this comment.
Yes, good suggestion. I'll do that.
No description provided.