feat: make repeat and while syntax builtin

[sgraf812]

This PR promotes the repeat, while, and repeat ... until parsers from syntax declarations in Init.While to @[builtin_doElem_parser] definitions in Lean.Parser.Do, alongside the other do-element parsers. The while variants and repeat ... until get @[builtin_macro] expansions; repeat itself gets a @[builtin_doElem_elab] so a follow-up can extend it with an option-driven choice between Loop.mk and a well-founded Repeat.mk.

The new builtin parsers are registered at low priority so that the bootstrapping syntax declarations in Init.While (still needed for stage0 compatibility) take precedence during the transition. After the next stage0 update, the Init.While syntax and macros can be removed.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 348ed9b3b0a8b0ac026dc9297e24bad6493631ec --onto fed2f32651e1e24a507c12aae234ac59e4d9916a. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-17 16:14:19)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 348ed9b3b0a8b0ac026dc9297e24bad6493631ec --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-04-17 16:14:21)