Nicer error message if `set_option` goes after doc string

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

If I do

/-- A comment that should go after `set_option` -/
set_option maxHeartbeats 10000 in
theorem simple : 0 = 0 := rfl

I get the confusing error message

unexpected token 'set_option'; expected 'abbrev', 'add_decl_doc', 'axiom', 'builtin_initialize', 'class', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'structure', 'syntax', 'theorem' or 'unif_hint'

which doesn't give any hints that the correct ordering is

set_option maxHeartbeats 10000 in
/-- A comment in the right place -/
theorem simple : 0 = 0 := rfl

Context

Zulip thread (which doesn't have any additional information): https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Confusing.20error.20message.20with.20set_option.20before.20doc.20comment/near/410865491

Steps to Reproduce

See above.

Expected behavior:

An error message that explains that set_option should go before the doc string, or at least hints in that direction.

Actual behavior:

The uninformative error message shown above.

Versions

• lean --version: Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)
• OS: macOS 14.1.2

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the example with Lean 4.5.0-rc1 and inspect the parser or diagnostic path handling a doc comment before set_option. Done means the reported error explains that set_option must precede the doc string, or provides a similarly useful hint, with coverage for the shown ordering.