error updates

jsiek · Dec 25, 2024 · 8341f67 · 8341f67
1 parent 5d50fea
commit 8341f67
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 3 deletions.
diff --git a/rec_desc_parser.py b/rec_desc_parser.py
@@ -793,7 +793,7 @@ def parse_proof_hi():
     for kw in proof_keywords:
         if edit_distance(token.value, kw) <= 2:
             error(meta_from_tokens(token, token),
-                  'did you mean "' + kw \
+                  'expected a proof.\nDid you mean "' + kw \
                   + '" instead of "' + current_token().value + '"?')
 
     try:

diff --git a/test/should-error/cases_error.pf.err b/test/should-error/cases_error.pf.err
@@ -1,4 +1,5 @@
-./test/should-error/cases_error.pf:5.5-5.9: did you mean "cases" instead of "case"?
+./test/should-error/cases_error.pf:5.5-5.9: expected a proof.
+Did you mean "have" instead of "case"?
 ./test/should-error/cases_error.pf:4.5-4.10: while parsing cases (use a logical or)
 	conclusion ::= "cases" proof case_list
 	case_list ::= case | case case_list

diff --git a/test/should-error/suffices_misspell.pf.err b/test/should-error/suffices_misspell.pf.err
@@ -1,3 +1,4 @@
-./test/should-error/suffices_misspell.pf:5.3-5.10: did you mean "suffices" instead of "sufices"?
+./test/should-error/suffices_misspell.pf:5.3-5.10: expected a proof.
+Did you mean "suffices" instead of "sufices"?
 ./test/should-error/suffices_misspell.pf:1.1-4.15: while parsing
 	proof_stmt ::= "theorem" identifier ":" formula "proof" proof "end"