add test not using _root_

src/Lean/Elab.lean

@@ -46,6 +46,7 @@ public import Lean.Elab.Notation
 public import Lean.Elab.Mixfix
 public import Lean.Elab.MacroRules
 public import Lean.Elab.BuiltinCommand
+public import Lean.Elab.Command.WithWeakNamespace
 public import Lean.Elab.BuiltinEvalCommand
 public import Lean.Elab.RecAppSyntax
 public import Lean.Elab.Eval

src/Lean/Elab/Command/WithWeakNamespace.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Daniel Selsam, Gabriel Ebner
+-/
+module
+
+prelude
+public import Lean.Elab.Command
+public import Lean.Data.OpenDecl
+
+namespace Lean.Elab.Command
+
+/-- Adds the name to the namespace, `_root_`-aware.
+```
+resolveNamespaceRelative `A `B.b == `A.B.b
+resolveNamespaceRelative `A `_root_.B.c == `B.c
+```
+-/
+def resolveNamespaceRelative (ns : Name) : Name → Name
+  | `_root_ => Name.anonymous
+  | Name.str n s .. => Name.mkStr (resolveNamespaceRelative ns n) s
+  | Name.num n i .. => Name.mkNum (resolveNamespaceRelative ns n) i
+  | Name.anonymous => ns
+
+/-- Changes the current namespace without causing scoped things to go out of scope -/
+def withWeakNamespace {α : Type} (ns : Name) (m : CommandElabM α) : CommandElabM α := do
+  let old ← getCurrNamespace
+  let ns := resolveNamespaceRelative old ns
+  modify fun s ↦ { s with env := s.env.registerNamespace ns }
+  modifyScope ({ · with currNamespace := ns })
+  try m finally modifyScope ({ · with currNamespace := old })
+
+@[builtin_command_elab Parser.Command.withWeakNamespace]
+def elabWithWeakNamespace : CommandElab
+  | `(Parser.Command.withWeakNamespace| with_weak_namespace $ns:ident $cmd) =>
+    withWeakNamespace ns.getId (elabCommand cmd)
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Command

src/Lean/Parser/Command.lean

@@ -314,6 +314,20 @@ corresponding `end <id>` or the end of the file.
 @[builtin_command_parser] def «namespace»    := leading_parser
   "namespace " >> checkColGt >> ident
 /--
+`with_weak_namespace <id> <cmd>` changes the current namespace to `<id>` for the duration of
+executing command `<cmd>`, without causing scoped things to go out of scope.
+
+This is in contrast to `namespace <id>` which pushes a new scope and deactivates scoped entries
+from the previous namespace. `with_weak_namespace` modifies the existing scope's namespace,
+so scoped extensions remain active.
+
+This is primarily useful for defining syntax extensions that should be scoped to a different
+namespace than the current one.
+-/
+@[builtin_command_parser] def withWeakNamespace := leading_parser
+  "with_weak_namespace " >> checkColGt >> ident >> ppSpace >> checkColGt >> commandParser
+
+/--
 `end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed
 with `end <id>`. The `end` command is optional at the end of a file.
 -/

tests/lean/run/withWeakNamespace.lean

@@ -0,0 +1,57 @@
+/-
+Tests for `with_weak_namespace` command
+-/
+
+-- Test 1: Basic absolute namespace usage
+namespace Foo
+
+def f : Nat := 1
+
+scoped infix:65 " + " => f
+
+with_weak_namespace _root_.Bar
+  def g : Nat := 2
+  #check 1 + 2  -- Scoped notation still works
+  #check Bar.g
+
+end Foo
+
+#check Bar.g
+#check Foo.f
+
+-- Test 2: _root_ handling
+namespace A.B
+
+with_weak_namespace _root_.C
+  def x : Nat := 1
+
+end A.B
+
+#check C.x
+
+-- Test 3: Scoped notation persists
+namespace Outer
+
+def outerDef : Nat := 5
+
+scoped infix:70 " * " => outerDef
+
+with_weak_namespace _root_.Test1
+  #check 1 * 2  -- Scoped notation from Outer still works
+
+end Outer
+
+-- Test 4: Relative namespace (without _root_)
+namespace Parent
+
+def parentFn (n : Nat) : Nat := n + 10
+
+scoped prefix:100 "!" => parentFn
+
+with_weak_namespace Child
+  def childDef : Nat := !0  -- Scoped notation from Parent still works
+  #check Parent.Child.childDef
+
+end Parent
+
+#check Parent.Child.childDef