chore: improve unexpected token messages

src/Lean/DocString/Parser.lean

@@ -255,7 +255,7 @@ private def strFn (str : String) : ParserFn := asStringFn <| fun c s =>
   let iniPos := s.pos
   let iniSz := s.stxStack.size
   let s := go str.startPos s
-  if s.hasError then s.mkErrorAt s!"'{str}'" iniPos (some iniSz) else s
+  if s.hasError then s.mkErrorAt s!"`{str}`" iniPos (some iniSz) else s
 
 /--
 Ordered lists may have two styles of indicator, with trailing dots or parentheses.
@@ -878,7 +878,7 @@ public def lookaheadOrderedListIndicator (ctxt : BlockCtxt) (p : OrderedListType
         | '.' => (s.next' c i h, (chFn ' ' <|> chFn '\n'), OrderedListType.numDot)
         | ')' => (s.next' c i h, (chFn ' ' <|> chFn '\n'), OrderedListType.parenAfter)
         | other =>
-          (s.setError { unexpected := s!"unexpected '{other}'", expected := ["'.'", "')'"] },
+          (s.setError { unexpected := s!"unexpected `{other}`", expected := ["`.`", "`)`"] },
            skipFn,
            .numDot)
       if s.hasError then {s with pos := iniPos}

src/Lean/Parser/Basic.lean

@@ -611,7 +611,7 @@ def rawFn (p : ParserFn) (trailingWs := false) : ParserFn := fun c s =>
   if s.hasError then s else rawAux startPos trailingWs c s
 
 def chFn (c : Char) (trailingWs := false) : ParserFn :=
-  rawFn (satisfyFn (fun d => c == d) ("'" ++ toString c ++ "'")) trailingWs
+  rawFn (satisfyFn (fun d => c == d) ("`" ++ toString c ++ "`")) trailingWs
 
 def rawCh (c : Char) (trailingWs := false) : Parser := {
   fn := chFn c trailingWs
@@ -1108,7 +1108,7 @@ def symbolInfo (sym : String) : ParserInfo := {
 }
 
 def symbolFn (sym : String) : ParserFn :=
-  symbolFnAux sym ("'" ++ sym ++ "'")
+  symbolFnAux sym ("`" ++ sym ++ "`")
 
 def symbolNoAntiquot (sym : String) : Parser :=
   let sym := sym.trimAscii.copy
@@ -1143,7 +1143,7 @@ def nonReservedSymbolFnAux (sym : String) (errorMsg : String) : ParserFn := fun
   s.mkUnexpectedTokenError errorMsg
 
 def nonReservedSymbolFn (sym : String) : ParserFn :=
-  nonReservedSymbolFnAux sym ("'" ++ sym ++ "'")
+  nonReservedSymbolFnAux sym ("`" ++ sym ++ "`")
 
 def nonReservedSymbolInfo (sym : String) (includeIdent : Bool) : ParserInfo := {
   firstTokens  :=
@@ -1232,7 +1232,7 @@ def unicodeSymbolInfo (sym asciiSym : String) : ParserInfo := {
 }
 
 def unicodeSymbolFn (sym asciiSym : String) : ParserFn :=
-  unicodeSymbolFnAux sym asciiSym ["'" ++ sym ++ "', '" ++ asciiSym ++ "'"]
+  unicodeSymbolFnAux sym asciiSym [s!"`{sym}`, `{asciiSym}`"]
 
 set_option linter.unusedVariables false in
 def unicodeSymbolNoAntiquot (sym asciiSym : String) (preserveForPP : Bool) : Parser :=
@@ -1311,7 +1311,7 @@ def identEqFn (id : Name) : ParserFn := fun c s =>
   if s.hasError then
     s
   else match s.stxStack.back with
-    | .ident _ _ val _ => if val != id then s.mkUnexpectedTokenError s!"identifier '{id}'" else s
+    | .ident _ _ val _ => if val != id then s.mkUnexpectedTokenError s!"identifier `{id}`" else s
     | _ => s.mkUnexpectedTokenError "identifier"
 
 def identEq (id : Name) : Parser := {

src/Lean/Parser/Module.lean

@@ -58,9 +58,31 @@ private partial def mkErrorMessage (c : InputContext) (pos : String.Pos.Raw) (st
       pos := r.start
       endPos? := some r.stop
     let unexpected := match e.unexpectedTk with
-      | .ident .. => "unexpected identifier"
-      | .atom _ v => s!"unexpected token '{v}'"
-      | _         => "unexpected token"  -- TODO: categorize (custom?) literals as well?
+      | .ident _ rawVal _ _ =>
+        s!"unexpected identifier `{toString rawVal}`"
+      | .atom _ v =>
+        s!"unexpected token `{v}`"
+      | .node _ k #[.atom _ v] =>
+        if k == numLitKind then
+          s!"unexpected numeral `{v}`"
+        else if k == strLitKind then
+          s!"unexpected string literal {v}"
+        else if k == charLitKind then
+          s!"unexpected character literal {v}"
+        else if k == scientificLitKind then
+          s!"unexpected scientific numeral `{v}`"
+        else if k == nameLitKind then
+          s!"unexpected name literal {v}"
+        else if k == fieldIdxKind then
+          s!"unexpected field index `{v}`"
+        else if k == hexnumKind then
+          s!"unexpected hexadecimal number `{v}`"
+        else if k == interpolatedStrLitKind then
+          s!"unexpected interpolated string fragment {v}"
+        else
+          s!"unexpected token `{v}`"
+      | _ =>
+        "unexpected token"
     e := { e with unexpected }
     -- 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

tests/lean/10488.lean.expected.out

@@ -11,24 +11,24 @@
 313e1 : Float
 10488.lean:16:11: error: missing exponent digits in scientific literal
 31.3 : Float
-10488.lean:18:11-18:12: error: unexpected identifier; expected command
+10488.lean:18:11-18:12: error: unexpected identifier `f`; expected command
 31.3 : Float
-10488.lean:19:11-19:13: error: unexpected identifier; expected command
+10488.lean:19:11-19:13: error: unexpected identifier `f2`; expected command
 31.3 : Float
-10488.lean:20:11-20:14: error: unexpected identifier; expected command
+10488.lean:20:11-20:14: error: unexpected identifier `ff2`; expected command
 10488.lean:22:7: error: unexpected identifier after decimal point; consider parenthesizing the number
 Nat.toDigits 11 13 : List Char
 ['1', '2']
 Nat.toDigits 11 : Nat → List Char
-10488.lean:25:20-25:21: error: unexpected token '('; expected command
+10488.lean:25:20-25:21: error: unexpected token `(`; expected command
 Nat.toDigits 11 13 : List Char
 foo.{u_1, u_2} {A : Sort u_1} {B : Sort u_2} : A → B → Unit
 10488.lean:30:11: error: unexpected identifier after decimal point; consider parenthesizing the number
 foo (Nat.succ 31) : ?m → Unit
 foo 31 : ?m → Unit
-10488.lean:32:13-32:14: error: unexpected token '('; expected command
+10488.lean:32:13-32:14: error: unexpected token `(`; expected command
 foo 31 : ?m → Unit
-10488.lean:33:15-33:16: error: unexpected token '('; expected command
+10488.lean:33:15-33:16: error: unexpected token `(`; expected command
 10488.lean:34:14-34:19: error(lean.invalidDottedIdent): Invalid dotted identifier notation: The expected type of `.succ` could not be determined
 
 Hint: Using one of these would be unambiguous:
@@ -39,12 +39,12 @@ Hint: Using one of these would be unambiguous:
 foo 31 sorry : Unit
 foo 31. succ : Unit
 11 : Nat
-10488.lean:37:9-37:13: error: unexpected identifier; expected command
+10488.lean:37:9-37:13: error: unexpected identifier `succ`; expected command
 10488.lean:38:7: error: unexpected identifier after decimal point; consider parenthesizing the number
 11.12 : Float
-10488.lean:39:12-39:16: error: unexpected identifier; expected command
+10488.lean:39:12-39:16: error: unexpected identifier `succ`; expected command
 10488.lean:40:8: error: unexpected identifier after decimal point; consider parenthesizing the number
-10488.lean:41:13-41:17: error: unexpected identifier; expected ')', ',' or ':'
+10488.lean:41:13-41:17: error: unexpected identifier `succ`; expected `)`, `,` or `:`
 bar.x.snd.snd : Nat
 { x := (2, 4, 1) }
 10488.lean:60:4-60:12: error: Invalid pattern: Expected a constructor or constant marked with `[match_pattern]`

tests/lean/1606.lean.expected.out

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

tests/lean/1760.lean.expected.out

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

tests/lean/1971.lean.expected.out

@@ -1,7 +1,7 @@
-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:36:11-36:12: error: unexpected token; expected command
-1971.lean:39:17-41:7: error: unexpected token 'example'; 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:36:11-36:12: error: unexpected numeral `0`; expected command
+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-3:25: error: unexpected token '⟩'; expected ')'
+348.lean:3:24-3:25: error: unexpected token `⟩`; expected `)`

tests/lean/361.lean.expected.out

@@ -1,10 +1,10 @@
-361.lean:1:62-3:7: error: unexpected token 'theorem'; 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
 h2 : p → q
 ⊢ q
-361.lean:6:0: error: unexpected end of input; expected '{'
+361.lean:6:0: error: unexpected end of input; expected `{`
 361.lean:5:11-5:13: error: unsolved goals
 p q r : Prop
 h2 : p → q

tests/lean/4117.lean.expected.out

@@ -1 +1 @@
-4117.lean:2:0: error: unexpected end of input; expected ')'
+4117.lean:2:0: error: unexpected end of input; expected `)`

tests/lean/4309.lean.expected.out

@@ -1 +1 @@
-4309.lean:3:7-3:9: error: unexpected token ':'; expected identifier
+4309.lean:3:7-3:9: error: unexpected token `:`; expected identifier

tests/lean/689.lean.expected.out

@@ -1,2 +1,2 @@
-689.lean:2:14-4:7: error: unexpected token 'section'; expected '|'
-689.lean:9:0: error: unexpected end of input; 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,12 +1,12 @@
-StxQuot.lean:8:12-8:13: error: unexpected token ')'; expected identifier or term
+StxQuot.lean:8:12-8:13: error: unexpected token `)`; expected identifier or term
 "`[email protected]._hyg.1"
 "<missing>"
 "<missing>"
 "<missing>"
 "(«term_+_» <missing> \"+\" (num \"1\"))"
 "(«term_+_» <missing> \"+\" (num \"1\"))"
 "(«term_+_» (num \"1\") \"+\" (num \"1\"))"
-StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
+StxQuot.lean:19:15-19:16: error: unexpected token `]`; expected term
 "(Term.fun \"fun\" (Term.basicFun [`[email protected]._hyg.1] [] \"=>\" `[email protected]._hyg.1))"
 "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [] [])\n (Command.definition\n  \"def\"\n  (Command.declId `[email protected]._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n  []))"
 "[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [] [])\n  (Command.definition\n   \"def\"\n   (Command.declId `[email protected]._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n   []))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [] [])\n  (Command.definition\n   \"def\"\n   (Command.declId `[email protected]._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (num \"2\") (Termination.suffix [] []) [])\n   []))]"

tests/lean/antiquotRecovery.lean.expected.out

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

tests/lean/byStrictIndent.lean.expected.out

@@ -1,6 +1,6 @@
 theorem byTopLevelNoIndent : ∀ (n : Nat), n > 1 → n > 1 :=
 fun n h => h
-byStrictIndent.lean:12:2: error: expected '{' or indented tactic sequence
+byStrictIndent.lean:12:2: error: expected `{` or indented tactic sequence
 byStrictIndent.lean:11:25-11:27: error: unsolved goals
 n : Nat
 h : n > 0
@@ -15,10 +15,10 @@ n : Nat
 h : n > 0
 helper : n > 1
 ⊢ n > 1
-byStrictIndent.lean:19:3-19:8: error: unexpected token 'sorry'; 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-25:11: error: unexpected token 'sorry'; expected command
+byStrictIndent.lean:25:6-25:11: error: unexpected token `sorry`; expected command

tests/lean/calcErrors.lean.expected.out

@@ -18,4 +18,4 @@ calcErrors.lean:40:7-40:12: error: invalid 'calc' step, left-hand side is
   γ : Sort u_1
 but previous right-hand side is
   b : β
-calcErrors.lean:60:18-60:19: error: unexpected token '['; expected command
+calcErrors.lean:60:18-60:19: error: unexpected token `[`; expected command

tests/lean/commandPrefix.lean.expected.out

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

tests/lean/decreasing_by.lean.expected.out

@@ -12,7 +12,7 @@ The basic measures relate at each recursive call as follows:
 1) 61:29-43 = ?
 2) 61:46-62 ? _
 Please use `termination_by` to specify a decreasing measure.
-decreasing_by.lean:75:13-77:3: error: unexpected token 'end'; expected '{' or tactic
+decreasing_by.lean:75:13-77:3: error: unexpected token `end`; expected `{` or tactic
 decreasing_by.lean:75:0-75:13: error: unsolved goals
 n m : Nat
 ⊢ Prod.Lex (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) (n, dec2 m) (n, m)

tests/lean/docparse/arg_0004.expected.out

@@ -1,4 +1,4 @@
-Failure @0 (⟨1, 0⟩): expected '(', '+', '-', expected identifier, string, or number or token
+Failure @0 (⟨1, 0⟩): expected `(`, `+`, `-`, expected identifier, string, or number or token
 Final stack:
   <missing>
 Remaining: "\n(x:=1)"

tests/lean/docparse/arg_0013.expected.out

@@ -1,5 +1,5 @@
 2 failures:
-  @7 (⟨1, 7⟩): expected ')'
+  @7 (⟨1, 7⟩): expected `)`
     ""
   @7 (⟨1, 7⟩): unterminated string literal
     ""

tests/lean/docparse/arg_0015.expected.out

@@ -1,7 +1,7 @@
 4 failures:
-  @4 (⟨1, 4⟩): expected ')'
+  @4 (⟨1, 4⟩): expected `)`
     ""
-  @4 (⟨1, 4⟩): expected ':='
+  @4 (⟨1, 4⟩): expected `:=`
     ""
   @4 (⟨1, 4⟩): expected token
     ""

tests/lean/docparse/arg_0016.expected.out

@@ -1,7 +1,7 @@
 3 failures:
-  @6 (⟨1, 6⟩): expected ')'
+  @6 (⟨1, 6⟩): expected `)`
     ""
-  @6 (⟨1, 6⟩): expected ':='
+  @6 (⟨1, 6⟩): expected `:=`
     ""
   @6 (⟨1, 6⟩): unexpected end of input
     ""

tests/lean/docparse/arg_0017.expected.out

@@ -1,4 +1,4 @@
-Failure @8 (⟨1, 8⟩): expected ')'
+Failure @8 (⟨1, 8⟩): expected `)`
 Final stack:
   (Lean.Doc.Syntax.named
    "("

tests/lean/docparse/arg_0018.expected.out

@@ -1,4 +1,4 @@
-Failure @8 (⟨1, 8⟩): expected ')'
+Failure @8 (⟨1, 8⟩): expected `)`
 Final stack:
   (Lean.Doc.Syntax.named
    "("

tests/lean/docparse/arg_val_0003.expected.out

@@ -1,4 +1,4 @@
-Failure @0 (⟨1, 0⟩): unexpected end of input; expected '(', '+' or '-'
+Failure @0 (⟨1, 0⟩): unexpected end of input; expected `(`, `+` or `-`
 Final stack:
   <missing>
 Remaining: ""

tests/lean/docparse/arg_val_0007.expected.out

@@ -1,4 +1,4 @@
-Failure @0 (⟨1, 0⟩): unterminated string literal; expected '(', '+', '-' or token
+Failure @0 (⟨1, 0⟩): unterminated string literal; expected `(`, `+`, `-` or token
 Final stack:
   (Lean.Doc.Syntax.arg_str <missing>)
 Remaining: "\"foo"

tests/lean/docparse/block_0007.expected.out

@@ -1,7 +1,7 @@
 2 failures:
   @36 (⟨3, 28⟩): expected token
     ""
-  @36 (⟨3, 28⟩): unexpected end of input; expected '![', '$$', '$', '[' or '[^'
+  @36 (⟨3, 28⟩): unexpected end of input; expected `![`, `$$`, `$`, `[^` or `[`
     ""
 
 Final stack:

tests/lean/docparse/block_0008.expected.out

@@ -1,7 +1,7 @@
 2 failures:
   @37 (⟨3, 28⟩): expected token
     ""
-  @37 (⟨3, 28⟩): unexpected end of input; expected '![', '$$', '$', '[' or '[^'
+  @37 (⟨3, 28⟩): unexpected end of input; expected `![`, `$$`, `$`, `[^` or `[`
     ""
 
 Final stack:

tests/lean/docparse/block_0009.expected.out

@@ -1,7 +1,7 @@
 2 failures:
   @44 (⟨4, 28⟩): expected token
     ""
-  @44 (⟨4, 28⟩): unexpected end of input; expected '![', '$$', '$', '[' or '[^'
+  @44 (⟨4, 28⟩): unexpected end of input; expected `![`, `$$`, `$`, `[^` or `[`
     ""
 
 Final stack:

tests/lean/docparse/block_0010.expected.out

@@ -1,7 +1,7 @@
 2 failures:
   @45 (⟨4, 28⟩): expected token
     ""
-  @45 (⟨4, 28⟩): unexpected end of input; expected '![', '$$', '$', '[' or '[^'
+  @45 (⟨4, 28⟩): unexpected end of input; expected `![`, `$$`, `$`, `[^` or `[`
     ""
 
 Final stack:

tests/lean/docparse/block_0011.expected.out

@@ -1,5 +1,5 @@
 2 failures:
-  @19 (⟨6, 0⟩): '{'; expected '![', '$$', '$', '[' or '[^'
+  @19 (⟨6, 0⟩): `{`; expected `![`, `$$`, `$`, `[^` or `[`
     "Here's a paragraph."
   @19 (⟨6, 0⟩): expected token
     "Here's a paragraph."

tests/lean/docparse/blocks_0007.expected.out

@@ -1,4 +1,4 @@
-Failure @2 (⟨2, 0⟩): ':'; expected %%% (at line beginning) or expected column at least 1
+Failure @2 (⟨2, 0⟩): `:`; expected %%% (at line beginning) or expected column at least 1
 Final stack:
   [(Lean.Doc.Syntax.ul
     "ul{"

tests/lean/docparse/blocks_0023.expected.out

@@ -1,4 +1,4 @@
-Failure @35 (⟨2, 15⟩): unexpected end of input; expected %%% (at line beginning), '![', '$$', '$', '[', '[^', beginning of line at ⟨2, 15⟩ or beginning of line or sequence of nestable block openers at ⟨2, 15⟩
+Failure @35 (⟨2, 15⟩): unexpected end of input; expected %%% (at line beginning), `![`, `$$`, `$`, `[^`, `[`, beginning of line at ⟨2, 15⟩ or beginning of line or sequence of nestable block openers at ⟨2, 15⟩
 Final stack:
   [(Lean.Doc.Syntax.dl
     "dl{"

tests/lean/docparse/blocks_0051.expected.out

@@ -1,4 +1,4 @@
-Failure @45 (⟨2, 29⟩): expected '(' or '['
+Failure @45 (⟨2, 29⟩): expected `(` or `[`
 Final stack:
   [(Lean.Doc.Syntax.para
     "para{"