perf: reduce Lean.Parser.Basic imports

src/Lean/Parser/Basic.lean

@@ -8,10 +8,7 @@ import Lean.Data.Position
 import Lean.Syntax
 import Lean.ToExpr
 import Lean.Environment
-import Lean.Attributes
 import Lean.Message
-import Lean.Compiler.InitAttr
-import Lean.ResolveName
 
 /-!
 # Basic Lean parser infrastructure
@@ -135,9 +132,6 @@ structure ParserContext extends InputContext, ParserModuleContext where
   savedPos?          : Option String.Pos := none
   forbiddenTk?       : Option Token := none
 
-def ParserContext.resolveName (ctx : ParserContext) (id : Name) : List (Name × List String) :=
-  ResolveName.resolveGlobalName ctx.env ctx.currNamespace ctx.openDecls id
-
 structure Error where
   unexpected : String := ""
   expected : List String := []

src/Lean/Parser/Extension.lean

@@ -622,6 +622,9 @@ def withOpenDeclFn (p : ParserFn) : ParserFn := fun c s =>
   fn   := withOpenDeclFn  p.fn
 }
 
+def ParserContext.resolveName (ctx : ParserContext) (id : Name) : List (Name × List String) :=
+  ResolveName.resolveGlobalName ctx.env ctx.currNamespace ctx.openDecls id
+
 def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s => Id.run do
   let stack := s.stxStack
   if stack.size < offset + 1 then