Incorrect parsing of non-indented `where` declaration followed by `declModifiers`

Prerequisites

• [ X ] Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• [ X ] Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• [ X ] Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Good afternoon! I have run into some strange behavior where an unindented where declaration will cause the next command to not be parsed correctly if it has declaration modifiers above it. Folks on Zulip believe that this may be caused by the modifier initially being parsed as belonging to another declaration in the current where, causing a def or similar keyword to be rejected due to it not backtracking.

Context

Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/Strange.20declaration.20parsing.20behavior/with/599627787

Context: I was working on some unrelated metaprogramming stuff.

Steps to Reproduce

def fun1 (x : Nat) : Nat :=
  aux1 x
where
aux1 (y : Nat) : Nat := y; -- Problem only if this isn't indented

/-- Everything works ok without a declModifier (doc comment, attribute, etc.) -/
def fun2 (x : Nat) : Nat := x -- unexpected token 'def'; expected '(', ':=', '|' or term

Expected behavior: fun2 should have been correctly parsed and elaborated.

Actual behavior: The parser throws an error when reaching the def keyword ("unexpected token 'def'; expected '(', ':=', '|' or term")

Versions

v4.31.0-rc1 (I used live.lean-lang.org)

Additional Information

N/A

Impact

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

Start by running the minimal example from the issue in live.lean-lang.org and confirm that the unindented where declaration followed by the documented modifier reproduces the parse error. Then trace the parser handling of where, declaration modifiers, and the following def. Done means the example parses and fun2 is correctly elaborated without regressing the existing syntax.