Optional nodes in `elab`

Stream: lean4

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

Is it a bug that the optional syntax node in TEST2 is resolved to none?

import Lean
open Lean

elab "TEST1" t:(term)? : term => do
  logInfo m!"t = {t}"
  return .sort .zero

elab "TEST2" t:("abc" term)? : term => do
  logInfo m!"t = {t}"
  return .sort .zero

elab "TEST3" t:optional("abc" term) : term => do
  logInfo m!"t = {t}"
  return .sort .zero

#check TEST1 10 -- t = some (10)

#check TEST2 abc 10 -- t = none

#check TEST3 abc 10 -- t = failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)

[Robin Arnez]

The reason why TEST2 produces none is that it uses docs#Lean.Syntax.getOptional? which returns none if there is more than one node inside (I guess otherwise it'd be ambiguous which node to take). And apparently ? is more special than optional since TEST3 just takes the raw syntax (["abc" (num "10")]) which the pretty-printer has no clue how to print.

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

I'd say there is at the very least an inconsistency with the docstring on ?. It goes "(p)? is shorthand for optional(p).", but that's not the case here. It might simply be a missing case in mkSyntaxAndPat.