Confusing error message with set_option before doc comment

Stream: lean4

[Geoffrey Irving]

If I do

/-- A comment that should go after the `set_option` -/
set_option maxHeartbeats 10000000 in
lemma simple : 7 = 7 := rfl

I get the confusing error message

unexpected token 'set_option'; expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'alias', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'declare_config_elab', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'irreducible_def', 'lemma', 'macro', 'macro_rules', 'notation', 'notation3', 'opaque', 'postfix', 'prefix', 'proof_wanted', 'register_builtin_option', 'register_label_attr', 'register_option', 'register_simp_attr', 'scoped', 'structure', 'syntax', 'theorem' or 'unif_hint'

After some searching, I finally realized that it was supposed to be

set_option maxHeartbeats 10000000 in
/-- A comment that should go after the `set_option` -/
lemma simple : 7 = 7 := rfl

Would it be possible for the error message to give more of a hint in that direction?

[Geoffrey Irving]

(deleted)

[Kim Morrison]

@Geoffrey Irving, could you open an issue for this?

[Geoffrey Irving]

^ Will do (later today)!

[Geoffrey Irving]

https://github.com/leanprover/lean4/issues/3135