`extractMacroScopes` incorrectly parses context component of names

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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

extractMacroScopes has not been updated to reflect the current syntax for the context part of macro scopes.

Old grammar:
<actual name>._@.(<ctx>.<scopes>)*.<ctx>._hyg.<scopes>

New grammar (for just the last <ctx>? for all of them?):
<main module>.<uniq>._hygCtx

It ends up breaking the name into parts incorrectly due to the presence of the <uniq> number in the context portion of the name.

Context

Discovered while reading the MacroM code at the end of Prelude.lean.

Steps to Reproduce

1. Create an ident Syntax using a syntax quotation.
2. Extract the Name from the ident, which should have macro scopes inserted.
3. Call Lean.extractMacroScopes on the Name value.
4. Inspect the ctx and imported fields of the resulting MacroScopesView value.

import Lean

open Lean Elab Command

#eval show CommandElabM _ from do
  let stx ← `(foo)
  let generatedName := stx.raw.getId
  logInfo s!"generatedName: {generatedName}"

  let parts := extractMacroScopes generatedName
  logInfo <|
    s!"Extracted MacroScopesView:" ++
    s!"\n  name:     {parts.name}" ++
    s!"\n  imported: {parts.imported}" ++
    s!"\n  ctx:      {parts.ctx}" ++
    s!"\n  scopes:   {parts.scopes}"

  let expectedCtx ← liftMacroM MonadQuotation.getContext
  if parts.ctx ≠ expectedCtx then
    logError s!"{parts.ctx} should be {expectedCtx}"
  if parts.imported ≠ .anonymous then
    logError s!"{parts.imported} should be Name.anonymous"

Expected behavior:
parts.imported should be Name.anonymous
parts.ctx should be <main module>.<uniq>._hygCtx

Actual behavior:
parts.imported is <main module>.<uniq>
parts.ctx is _hygCtx

Versions

4.29.0
4.30.0-nightly-2026-03-30

Additional Information

Impact

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

Start by reading extractMacroScopes and the MacroM code at the end of Prelude.lean, then run the minimal Lean example from the issue to inspect the parsed fields. The fix is complete when the generated name yields Name.anonymous for imported and the full <main module>.<uniq>._hygCtx value for ctx.