fix: end_local_scope does not work with compound namespace names

src/Lean/Elab/BuiltinCommand.lean

@@ -116,8 +116,9 @@ private def checkEndHeader : Name → List Scope → Option Name
       addScope (isNewNamespace := false) (isNoncomputable := ncTk.isSome) (isPublic := publicTk.isSome) (isMeta := metaTk.isSome) (attrs := attrs) "" (← getCurrNamespace)
   | _                        => throwUnsupportedSyntax
 
-@[builtin_command_elab InternalSyntax.end_local_scope] def elabEndLocalScope : CommandElab := fun _ => do
-  setDelimitsLocal
+@[builtin_command_elab InternalSyntax.end_local_scope] def elabEndLocalScope : CommandElab := fun stx => do
+  let depth := stx[1].toNat
+  setDelimitsLocal depth
 
 /--
 Produces a `Name` composed of the names of at most the innermost `n` scopes in `ss`, truncating if an
@@ -528,7 +529,7 @@ open Lean.Parser.Command.InternalSyntax in
 @[builtin_macro Lean.Parser.Command.«in»] def expandInCmd : Macro
   | `($cmd₁ in%$tk $cmd₂) =>
     -- Limit ref variability for incrementality; see Note [Incremental Macros]
-    withRef tk `(section $cmd₁:command $endLocalScopeSyntax:command $cmd₂ end)
+    withRef tk `(section $cmd₁:command $(endLocalScopeSyntax 1):command $cmd₂ end)
   | _                 => Macro.throwUnsupported
 
 @[builtin_command_elab Parser.Command.addDocString] def elabAddDeclDoc : CommandElab := fun stx => do

src/Lean/Elab/Declaration.lean

@@ -152,8 +152,9 @@ def expandNamespacedDeclaration : Macro := fun stx => do
   | some (ns, newStx) => do
     -- Limit ref variability for incrementality; see Note [Incremental Macros]
     let declTk := stx[1][0]
+    let depth := ns.getNumParts
     let ns := mkIdentFrom declTk ns
-    withRef declTk `(namespace $ns $endLocalScopeSyntax:command $(⟨newStx⟩) end $ns)
+    withRef declTk `(namespace $ns $(endLocalScopeSyntax depth):command $(⟨newStx⟩) end $ns)
   | none => Macro.throwUnsupported
 
 @[builtin_command_elab declaration, builtin_incremental]

src/Lean/Parser/Command.lean

@@ -342,10 +342,11 @@ namespace InternalSyntax
   This command is for internal use only. It is intended for macros that implicitly introduce new
   scopes, such as `expandInCmd` and `expandNamespacedDeclaration`. It allows local attributes to remain
   accessible beyond those implicit scopes, even though they would normally be hidden from the user.
+  The numeric argument specifies how many scope levels to mark as non-delimiting.
   -/
-  scoped syntax (name := end_local_scope) "end_local_scope" : command
+  scoped syntax (name := end_local_scope) "end_local_scope" num : command
 
-  def endLocalScopeSyntax : Command := Unhygienic.run `(end_local_scope)
+  def endLocalScopeSyntax (depth : Nat) : Command := Unhygienic.run `(end_local_scope $(Syntax.mkNumLit (toString depth)))
 end InternalSyntax
 
 /-- Declares one or more typed variables, or modifies whether already-declared variables are

src/Lean/ScopedEnvExtension.lean

@@ -144,13 +144,18 @@ def ScopedEnvExtension.popScope (ext : ScopedEnvExtension α β σ) (env : Envir
     | _      :: state₂ :: stack => { s with stateStack := state₂ :: stack }
     | _ => s
 
-/-- Modifies `delimitsLocal` flag to `false` to turn off delimiting of local entries.
+/-- Modifies `delimitsLocal` flag to `false` on the top `depth` entries of the state stack,
+to turn off delimiting of local entries across multiple implicit scope levels
+(e.g. those introduced by compound `namespace A.B.C` expansions).
 -/
-def ScopedEnvExtension.setDelimitsLocal (ext : ScopedEnvExtension α β σ) (env : Environment)  : Environment :=
+def ScopedEnvExtension.setDelimitsLocal (ext : ScopedEnvExtension α β σ) (env : Environment) (depth : Nat) : Environment :=
   ext.ext.modifyState (asyncMode := .local) env fun s =>
-    match s.stateStack with
-    | [] => s
-    | state :: stack => {s with stateStack := {state with delimitsLocal := false} :: stack}
+    {s with stateStack := go depth s.stateStack}
+where
+  go : Nat → List (State σ) → List (State σ)
+    | 0, stack => stack
+    | _, [] => []
+    | n + 1, state :: stack => {state with delimitsLocal := false} :: go n stack
 
 def ScopedEnvExtension.addEntry (ext : ScopedEnvExtension α β σ) (env : Environment) (b : β) : Environment :=
   ext.ext.addEntry env (Entry.global b)
@@ -226,11 +231,12 @@ def popScope [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] : m Unit :=
   for ext in (← scopedEnvExtensionsRef.get) do
     modifyEnv ext.popScope
 
-/-- Used to implement `end_local_scope` command, that disables delimiting local entries of ScopedEnvExtension in a current scope.
+/-- Used to implement `end_local_scope` command, that disables delimiting local entries of ScopedEnvExtension
+across `depth` scope levels.
 -/
-def setDelimitsLocal [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] : m Unit := do
+def setDelimitsLocal [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] (depth : Nat) : m Unit := do
   for ext in (← scopedEnvExtensionsRef.get) do
-    modifyEnv (ext.setDelimitsLocal ·)
+    modifyEnv (ext.setDelimitsLocal · depth)
 
 def activateScoped [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] (namespaceName : Name) : m Unit := do
   for ext in (← scopedEnvExtensionsRef.get) do

tests/elab/13268.lean

@@ -0,0 +1,9 @@
+local macro (name := hi) "test1" : term => `(42)
+local macro (name := hi.there) "test2" : term => `(42)
+local macro (name := hi.there.more) "test3" : term => `(42)
+local macro (name := hi.there.more.yes) "test4" : term => `(42)
+
+#check test1
+#check test2
+#check test3
+#check test4

tests/elab/13268.lean.out.expected

@@ -0,0 +1,4 @@
+42 : Nat
+42 : Nat
+42 : Nat
+42 : Nat