Parse issue involving try-catch-catch

example : IO Unit := do
  try
    for _ in [1] do
      try
        pure ()
      catch _ => unreachable!
  catch _ => unreachable!

produces the error invalid `try`, it must have a `catch` or `finally` , tested on 4.20.0-rc2. It appears the issue is that it is parsed as a try-catch-catch block like this:

example : IO Unit := do
  try
    for _ in [1] do
      try
        pure ()
      catch _ => unreachable!
      catch _ => unreachable!

and so the first try is left orphaned. (Are multiple catch blocks like this actually used in practice? I would not expect this to be legal even without the weird indentation.)

Start by reproducing the example with Lean 4.20.0-rc2 and inspect how the parser handles the nested try and catch indentation. Confirm the intended parsing behavior, then verify that the example no longer produces the invalid-try error and that multiple catch blocks remain handled appropriately.