refactor: move Synax.hasIdent, shake dependencies

src/Lean/Compiler/LCNF/Main.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Compiler.Options
+import Lean.Compiler.ExternAttr
 import Lean.Compiler.LCNF.PassManager
 import Lean.Compiler.LCNF.Passes
 import Lean.Compiler.LCNF.PrettyPrinter

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.PrettyPrinter
+import Lean.PrettyPrinter.Delaborator.Options
 import Lean.Compiler.LCNF.CompilerM
 import Lean.Compiler.LCNF.Internalize
 

src/Lean/Elab/BuiltinCommand.lean

@@ -11,7 +11,6 @@ import Lean.Elab.Eval
 import Lean.Elab.Command
 import Lean.Elab.Open
 import Lean.Elab.SetOption
-import Lean.PrettyPrinter
 
 namespace Lean.Elab.Command
 

src/Lean/Elab/PreDefinition/TerminationArgument.lean

@@ -10,7 +10,7 @@ import Lean.Elab.Term
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.PreDefinition.TerminationHint
-import Lean.PrettyPrinter.Delaborator
+import Lean.PrettyPrinter.Delaborator.Basic
 
 /-!
 This module contains
@@ -115,7 +115,7 @@ def TerminationArgument.delab (arity : Nat) (extraParams : Nat) (termArg : Termi
       -- any variable not mentioned syntatically (it may appear in the `Expr`, so do not just use
       -- `e.bindingBody!.hasLooseBVar`) should be delaborated as a hole.
       let vars  : TSyntaxArray [`ident, `Lean.Parser.Term.hole] :=
-        Array.map (fun (i : Ident) => if hasIdent i.getId stxBody then i else hole) vars
+        Array.map (fun (i : Ident) => if stxBody.raw.hasIdent i.getId then i else hole) vars
       -- drop trailing underscores
       let mut vars := vars
       while ! vars.isEmpty && vars.back.raw.isOfKind ``hole do vars := vars.pop

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -769,16 +769,6 @@ def delabMData : Delab := do
   else
     withMDataOptions delab
 
-/--
-Check for a `Syntax.ident` of the given name anywhere in the tree.
-This is usually a bad idea since it does not check for shadowing bindings,
-but in the delaborator we assume that bindings are never shadowed.
--/
-partial def hasIdent (id : Name) : Syntax → Bool
-  | Syntax.ident _ _ id' _ => id == id'
-  | Syntax.node _ _ args   => args.any (hasIdent id)
-  | _                      => false
-
 /--
 Return `true` iff current binder should be merged with the nested
 binder, if any, into a single binder group:
@@ -824,7 +814,7 @@ def delabLam : Delab :=
     let e ← getExpr
     let stxT ← withBindingDomain delab
     let ppTypes ← getPPOption getPPFunBinderTypes
-    let usedDownstream := curNames.any (fun n => hasIdent n.getId stxBody)
+    let usedDownstream := curNames.any (fun n => stxBody.hasIdent n.getId)
 
     -- leave lambda implicit if possible
     -- TODO: for now we just always block implicit lambdas when delaborating. We can revisit.

src/Lean/Syntax.lean

@@ -164,6 +164,16 @@ def asNode : Syntax → SyntaxNode
 def getIdAt (stx : Syntax) (i : Nat) : Name :=
   (stx.getArg i).getId
 
+/--
+Check for a `Syntax.ident` of the given name anywhere in the tree.
+This is usually a bad idea since it does not check for shadowing bindings,
+but in the delaborator we assume that bindings are never shadowed.
+-/
+partial def hasIdent (id : Name) : Syntax → Bool
+  | ident _ _ id' _ => id == id'
+  | node _ _ args   => args.any (hasIdent id)
+  | _               => false
+
 @[inline] def modifyArgs (stx : Syntax) (fn : Array Syntax → Array Syntax) : Syntax :=
   match stx with
   | node i k args => node i k (fn args)

src/Lean/Widget/InteractiveCode.lean

@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
 prelude
-import Lean.PrettyPrinter
 import Lean.Server.Rpc.Basic
 import Lean.Server.InfoUtils
 import Lean.Widget.TaggedText