Should try/catch be whitespace-sensitive?

Stream: lean4 dev

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

It caught me off-guard that the following example doesn't parse:

example : Option Nat := do
  try
    try
      return 0
    catch _ =>
      return 0
  catch _ =>
    return 0

It does work with some parenthesization:

example : Option Nat := do
  try
    (try
      return 0
    catch _ =>
      return 0)
  catch _ =>
    return 0

[Mario Carneiro]

lean#8220