Fix a grammar panic (#75)

metamath · Mar 6, 2022 · 0dbd297 · 0dbd297
1 parent 0d57450
commit 0dbd297
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 6 deletions.
diff --git a/src/diag.rs b/src/diag.rs
@@ -170,7 +170,7 @@ pub enum Diagnostic {
     NotAProvableStatement,
     OldAltNotDiscouraged,
     ParenOrderError(Span, Span),
-    ParsedStatementTooShort(Token),
+    ParsedStatementTooShort(Option<Token>),
     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
@@ -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