diff --git a/src/diag.rs b/src/diag.rs index a68d396..c0b5f8e 100644 --- a/src/diag.rs +++ b/src/diag.rs @@ -170,7 +170,7 @@ pub enum Diagnostic { NotAProvableStatement, OldAltNotDiscouraged, ParenOrderError(Span, Span), - ParsedStatementTooShort(Token), + ParsedStatementTooShort(Option), ParsedStatementNoTypeCode, ParsedStatementWrongTypeCode(Token), ProofDvViolation, @@ -831,9 +831,12 @@ impl Diagnostic { later, )]) } - ParsedStatementTooShort(ref tok) => ("Parsed statement too short".into(), vec![( + ParsedStatementTooShort(ref opt_tok) => ("Parsed statement too short".into(), vec![( AnnotationType::Error, - format!("Statement is too short, expecting for example {expected}", expected = t(tok)).into(), + match opt_tok { + Some(tok) => format!("Statement is too short, expecting for example {expected}", expected = t(tok)).into(), + None => "Statement is too short, and does not correspond to any valid prefix".into(), + }, stmt, stmt.span(), )]), diff --git a/src/grammar.rs b/src/grammar.rs index e8d2c73..c4f78ba 100644 --- a/src/grammar.rs +++ b/src/grammar.rs @@ -459,9 +459,11 @@ impl Grammar { } fn too_short(map: &HashMap<(SymbolType, Atom), NextNode>, nset: &Nameset) -> Diagnostic { - let expected_symbol = map.keys().find(|k| k.0 == SymbolType::Constant).unwrap().1; - let expected_token = nset.atom_name(expected_symbol).into(); - Diagnostic::ParsedStatementTooShort(expected_token) + Diagnostic::ParsedStatementTooShort( + map.keys() + .find(|k| k.0 == SymbolType::Constant) + .map(|(_, expected_symbol)| nset.atom_name(*expected_symbol).into()), + ) } /// Gets the map of a branch