/-!
  # More helpful ranges of parser error messages on unexpected tokens

  When the parser hits an unexpected token, it will now include all preceding
  whitespace in the error message range as the expected token could be inserted
  at any of these places to fix the error. -/

/-!
  In the following example, we want the parser error to start right after
  `exact` as the error belongs to this declaration, not the next one, and
  otherwise would be too easy to overlook. -/

theorem lem1 : True := by
  exact

theorem lem2 : True := ⟨⟩

/-!
  Outside of tactics as well it is generally a better idea to place the error
  right after the last correct token. -/

def f1

def f2 := 0

/-!
  We do not currently special-case linebreaks in this; on a single line,
  the shift is usually not very noticeable nor clearly worse than before. -/

def f3 := def f4 := 0

/-! Test other expected token errors as well -/

inductive

example := 0

-- merge of token errors
set_option pp.all

example := 0

/-! Do not shift other kinds of errors. -/

example := "a