feat: include unexpected token in error message

src/Lean/Parser/Module.lean

@@ -34,7 +34,9 @@ structure ModuleParserState where
 
 private def mkErrorMessage (c : InputContext) (s : ParserState) (e : Parser.Error) : Message := Id.run do
   let mut pos := c.fileMap.toPosition s.pos
-  if e.stopPos?.isSome then
+  -- if there is an unexpected token, include preceding whitespace as well as the expected token could
+  -- be inserted at any of these places to fix the error; see tests/lean/1971.lean
+  if !e.unexpected.isEmpty && e.stopPos?.isSome then
     if let .original (trailing := trailing) .. := s.stxStack.back.getTailInfo then
       if trailing.stopPos == s.pos then
         pos := c.fileMap.toPosition trailing.startPos

src/Lean/Parser/Types.lean

@@ -293,7 +293,11 @@ def mkErrorAt (s : ParserState) (msg : String) (pos : String.Pos) (initStackSz?
 def mkUnexpectedTokenErrors (s : ParserState) (ex : List String) : ParserState :=
   let tk := s.stxStack.back
   let s := s.setPos tk.getPos?.get!
-  let s := s.setError { stopPos? := tk.getTailPos?, expected := ex }
+  let unexpected := match tk with
+    | .ident .. => "unexpected identifier"
+    | .atom _ v => s!"unexpected token '{v}'"
+    | _         => "unexpected token"  -- TODO: categorize (custom?) literals as well?
+  let s := s.setError { stopPos? := tk.getTailPos?, expected := ex, unexpected }
   s.popSyntax.pushSyntax .missing
 
 /--

tests/lean/1606.lean.expected.out

@@ -1,9 +1,9 @@
 1606.lean:1:18-2:6: error: unsolved goals
 ⊢ True
-1606.lean:3:4: error: expected command
+1606.lean:3:4-3:8: error: unexpected identifier; expected command
 1606.lean:8:18-10:8: error: unsolved goals
 ⊢ True
-1606.lean:11:4: error: expected command
+1606.lean:11:4-11:14: error: unexpected identifier; expected command
 1606.lean:19:18-21:14: error: unsolved goals
 ⊢ True
-1606.lean:22:4: error: expected command
+1606.lean:22:4-22:14: error: unexpected identifier; expected command

tests/lean/1705.lean.expected.out

@@ -2,4 +2,4 @@
   T
 term has type
   ?m
-1705.lean:1:18: error: expected command
+1705.lean:1:18-1:19: error: unexpected identifier; expected command

tests/lean/1707.lean.expected.out

@@ -1,2 +1,2 @@
 1707.lean:1:9-1:12: error: invalid field index
-1707.lean:1:12: error: expected command
+1707.lean:1:12-1:13: error: unexpected identifier; expected command

tests/lean/1760.lean.expected.out

@@ -1,2 +1,2 @@
-1760.lean:3:0: error: expected ':', ']' or term
+1760.lean:2:31-3:6: error: unexpected token '#check'; expected ':', ']' or term
 () : Unit

tests/lean/1971.lean

@@ -39,3 +39,7 @@ example := 0
 set_option pp.all
 
 example := 0
+
+/-! Do not shift other kinds of errors. -/
+
+example := "a

tests/lean/1971.lean.expected.out

@@ -1,5 +1,6 @@
-1971.lean:14:7-16:7: error: expected term
-1971.lean:22:6-24:3: error: expected ':=', 'where' or '|'
-1971.lean:30:9-30:13: error: expected term
-1971.lean:34:9-36:7: error: expected identifier
-1971.lean:39:17-41:7: error: expected 'false', 'true', numeral or string literal
+1971.lean:14:7-16:7: error: unexpected token 'theorem'; expected term
+1971.lean:22:6-24:3: error: unexpected token 'def'; expected ':=', 'where' or '|'
+1971.lean:30:9-30:13: error: unexpected token 'def'; expected term
+1971.lean:34:9-36:7: error: unexpected token 'example'; expected identifier
+1971.lean:39:17-41:7: error: unexpected token 'example'; expected 'false', 'true', numeral or string literal
+1971.lean:45:11: error: unterminated string literal

tests/lean/348.lean.expected.out

@@ -1 +1 @@
-348.lean:3:24: error: expected ')'
+348.lean:3:24-3:25: error: unexpected token '⟩'; expected ')'

tests/lean/361.lean.expected.out

@@ -1,4 +1,4 @@
-361.lean:3:0: error: expected '{' or tactic
+361.lean:1:62-3:7: error: unexpected token 'theorem'; expected '{' or tactic
 361.lean:1:60-1:62: error: unsolved goals
 p q r : Prop
 h1 : p ∨ q

tests/lean/689.lean.expected.out

@@ -1,2 +1,2 @@
-689.lean:4:0: error: expected '|'
+689.lean:2:14-4:7: error: unexpected token 'section'; expected '|'
 689.lean:9:0: error: unexpected end of input; expected '{'

tests/lean/StxQuot.lean.expected.out

@@ -1,4 +1,4 @@
-StxQuot.lean:8:12: error: expected identifier or term
+StxQuot.lean:8:12-8:13: error: unexpected token ')'; expected identifier or term
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "<missing>"
 "<missing>"
@@ -6,7 +6,7 @@ StxQuot.lean:8:12: error: expected identifier or term
 "(«term_+_» <missing> \"+\" (num \"1\"))"
 "(«term_+_» <missing> \"+\" (num \"1\"))"
 "(«term_+_» (num \"1\") \"+\" (num \"1\"))"
-StxQuot.lean:19:15: error: expected term
+StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] [] \"=>\" `a._@.UnhygienicMain._hyg.1))"
 "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") [])\n  []\n  []\n  []))"
 "[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") [])\n   []\n   []\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") [])\n   []\n   []\n   []))]"

tests/lean/antiquotRecovery.lean.expected.out

@@ -1 +1 @@
-antiquotRecovery.lean:5:18: error: expected ')'
+antiquotRecovery.lean:5:17-5:19: error: unexpected token '$'; expected ')'

tests/lean/byStrictIndent.lean.expected.out

@@ -15,10 +15,10 @@ n : Nat
 h : n > 0
 helper : n > 1
 ⊢ n > 1
-byStrictIndent.lean:19:3: error: expected command
+byStrictIndent.lean:19:3-19:8: error: unexpected token 'sorry'; expected command
 byStrictIndent.lean:22:54-24:9: error: unsolved goals
 n : Nat
 h : n > 0
 helper : n > 1
 ⊢ n > 1
-byStrictIndent.lean:25:6: error: expected command
+byStrictIndent.lean:25:6-25:11: error: unexpected token 'sorry'; expected command

tests/lean/commandPrefix.lean.expected.out

@@ -1,3 +1,3 @@
 let_fun this := ();
 this : Id Unit
-commandPrefix.lean:3:0: error: expected command
+commandPrefix.lean:3:0-3:4: error: unexpected identifier; expected command

tests/lean/exitAfterParseError.lean.expected.out

@@ -1,2 +1,2 @@
-exitAfterParseError.lean:5:0: error: expected ':=', 'where' or '|'
+exitAfterParseError.lean:3:7-5:5: error: unexpected token '#exit'; expected ':=', 'where' or '|'
 exitAfterParseError.lean:5:0-5:5: warning: using 'exit' to interrupt Lean

tests/lean/have.lean.expected.out

@@ -1,4 +1,4 @@
-have.lean:4:0: error: expected term
+have.lean:2:19-4:7: error: unexpected token 'example'; expected term
 have.lean:2:18-2:19: error: don't know how to synthesize placeholder
 context:
 ⊢ False

tests/lean/letArrowOutsideDo.lean.expected.out

@@ -1 +1 @@
-letArrowOutsideDo.lean:2:8: error: expected ':=' or '|'
+letArrowOutsideDo.lean:2:7-2:9: error: unexpected token '←'; expected ':=' or '|'

tests/lean/linterUnusedVariables.lean.expected.out

@@ -38,7 +38,7 @@ a : Nat
 ⊢ Nat
 linterUnusedVariables.lean:227:0-227:7: warning: declaration uses 'sorry'
 linterUnusedVariables.lean:228:0-228:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:231:0: error: expected '{' or tactic
+linterUnusedVariables.lean:229:29-231:7: error: unexpected token 'theorem'; expected '{' or tactic
 linterUnusedVariables.lean:229:27-229:29: error: unsolved goals
 bar : ?m
 bar' : Nat → Nat

tests/lean/nonReserved.lean.expected.out

@@ -1,2 +1,2 @@
 10 : Nat
-nonReserved.lean:11:11: error: expected 'bla'
+nonReserved.lean:11:10-11:14: error: unexpected identifier; expected 'bla'

tests/lean/partialVariable.lean.expected.out

@@ -1 +1 @@
-partialVariable.lean:1:9: error: expected '(', '[', '{' or '⦃'
+partialVariable.lean:1:8-1:10: error: unexpected token ':'; expected '(', '[', '{' or '⦃'

tests/lean/precissues.lean.expected.out

@@ -4,9 +4,9 @@ f 1 fun x => x : Nat
 0 : Nat
 f 1 fun x => x : Nat
 id.{u} {α : Sort u} (a : α) : α
-precissues.lean:15:10: error: expected command
+precissues.lean:15:10-15:14: error: unexpected token 'have'; expected command
 id.{u} {α : Sort u} (a : α) : α
-precissues.lean:17:10: error: expected command
+precissues.lean:17:10-17:13: error: unexpected token 'let'; expected command
 1 : Nat
 id
   (let_fun this := True.intro;
@@ -27,4 +27,4 @@ p ∧ ¬q : Prop
 id ¬p : Prop
 Nat → ∀ (a : Nat), a = a : Prop
 id.{u} {α : Sort u} (a : α) : α
-precissues.lean:41:10: error: expected command
+precissues.lean:41:10-41:14: error: unexpected token 'foo!'; expected command

tests/lean/scientific.lean.expected.out

@@ -9,11 +9,11 @@
 123000.000000
 -8.534000
 scientific.lean:14:6-14:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)
-scientific.lean:14:7: error: expected command
+scientific.lean:14:7-14:10: error: unexpected token; expected command
 scientific.lean:15:6-15:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)
-scientific.lean:15:7: error: expected command
+scientific.lean:15:7-15:12: error: unexpected token; expected command
 scientific.lean:16:6-16:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)
-scientific.lean:16:7: error: expected command
+scientific.lean:16:7-16:16: error: unexpected token; expected command
 scientific.lean:19:6-19:7: error: unknown identifier 'e'
 scientific.lean:19:0-19:9: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
 scientific.lean:20:9: error: missing exponent digits in scientific literal

tests/lean/semicolonOrLinebreak.lean.expected.out

@@ -1,4 +1,4 @@
 semicolonOrLinebreak.lean:2:12: error: expected ';' or line break
 semicolonOrLinebreak.lean:9:31-10:8: error: fields missing: 'y'
-semicolonOrLinebreak.lean:10:8: error: expected command
-semicolonOrLinebreak.lean:20:8: error: expected ':'
+semicolonOrLinebreak.lean:10:8-10:9: error: unexpected identifier; expected command
+semicolonOrLinebreak.lean:20:7-20:9: error: unexpected token '}'; expected ':'

tests/lean/syntaxPrec.lean.expected.out

@@ -1,4 +1,4 @@
-syntaxPrec.lean:1:18: error: expected ':'
+syntaxPrec.lean:1:17-1:21: error: unexpected token '<|>'; expected ':'
 [Elab.command] syntax "foo" ("*" <|> term,+) : term
   [Elab.command] @[term_parser 1000]
       def «termFoo*_» : Lean.ParserDescr✝ :=