RFC: distinguish parser errors and elaboration errors

Proposal

At the moment, kernel errors are reported with a prefix (kernel), but syntax/parser errors and elaboration errors require some amount of understanding to distinguish.
I propose to prefix syntax errors with (parser) or (syntax).

Example:

import Mathlib

example 1 + 2 = 3 := by rfl

gives the error

unexpected token; expected ':=', 'where' or '|'

and I suggest it should instead give the error

(syntax) unexpected token; expected ':=', 'where' or '|'

Motivation

• This error matches the existing structure for kernel errors.
• The presence of this extra tag helps new users to understand the source of their error at a glance, without needing to be familiar with jargon (eg "token")
• It would be nice to additionally have clearer errors around macro expansion, but for now I am happy to leave that out of the proposal.

Comments

• User Experience: Primarily this makes the error messages more informative for new users, with virtually no negative for experienced users.

• Beneficiaries: Students are often confused by Lean's error messages, in particular it is sometimes not clear to them whether an error comes from mis-writing syntax, or from a tactic failure. While experienced users can tell the error source from understanding the error, beginners often struggle to parse and understand error messages, in particular parsing/syntax errors.

• Maintainability: This should be a very minor change to error messages.

No files or tests are named. Start by locating Lean 4's parser and syntax-error reporting, then compare it with the existing kernel error prefix handling. Done means syntax or parser errors consistently include the proposed prefix and the example reports the tagged message without changing elaboration or kernel errors.