fix: include references in attributes in call hierarchy (#5650)

By ensuring all `declModifiers` are included in `addDeclarationRanges`,
`implementedBy` references etc are included in the call hierarchy

src/Lean/Elab/BuiltinCommand.lean

@@ -16,12 +16,13 @@ import Lean.Elab.SetOption
 namespace Lean.Elab.Command
 
 @[builtin_command_elab moduleDoc] def elabModuleDoc : CommandElab := fun stx => do
-   match stx[1] with
-   | Syntax.atom _ val =>
-     let doc := val.extract 0 (val.endPos - ⟨2⟩)
-     let range ← Elab.getDeclarationRange stx
-     modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
-   | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
+  match stx[1] with
+  | Syntax.atom _ val =>
+    let doc := val.extract 0 (val.endPos - ⟨2⟩)
+    let some range ← Elab.getDeclarationRange? stx
+      | return  -- must be from partial syntax, ignore
+    modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
+  | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
 
 private def addScope (isNewNamespace : Bool) (isNoncomputable : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do
   modify fun s => { s with

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -84,7 +84,7 @@ private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorr
   -- An alternative design would be to make `elabTermForEval` into a term elaborator and elaborate the command all at once
   -- with `unsafe def _eval := term_for_eval% $t`, which we did try, but unwanted error messages
   -- such as "failed to infer definition type" can surface.
-  let defView := mkDefViewOfDef { isUnsafe := true }
+  let defView := mkDefViewOfDef { isUnsafe := true, stx := ⟨.missing⟩ }
     (← `(Parser.Command.definition|
           def $(mkIdent <| `_root_ ++ declName) := $(← Term.exprToSyntax value)))
   Term.elabMutualDef #[] { header := "" } #[defView]

src/Lean/Elab/DeclModifiers.lean

@@ -57,6 +57,7 @@ inductive RecKind where
 
 /-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...). -/
 structure Modifiers where
+  stx             : TSyntax ``Parser.Command.declModifiers
   docString?      : Option String := none
   visibility      : Visibility := Visibility.regular
   isNoncomputable : Bool := false
@@ -121,16 +122,16 @@ section Methods
 variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m]
 
 /-- Elaborate declaration modifiers (i.e., attributes, `partial`, `private`, `protected`, `unsafe`, `noncomputable`, doc string)-/
-def elabModifiers (stx : Syntax) : m Modifiers := do
-  let docCommentStx := stx[0]
-  let attrsStx      := stx[1]
-  let visibilityStx := stx[2]
-  let noncompStx    := stx[3]
-  let unsafeStx     := stx[4]
+def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers := do
+  let docCommentStx := stx.raw[0]
+  let attrsStx      := stx.raw[1]
+  let visibilityStx := stx.raw[2]
+  let noncompStx    := stx.raw[3]
+  let unsafeStx     := stx.raw[4]
   let recKind       :=
-    if stx[5].isNone then
+    if stx.raw[5].isNone then
       RecKind.default
-    else if stx[5][0].getKind == ``Parser.Command.partial then
+    else if stx.raw[5][0].getKind == ``Parser.Command.partial then
       RecKind.partial
     else
       RecKind.nonrec
@@ -148,7 +149,7 @@ def elabModifiers (stx : Syntax) : m Modifiers := do
     | none       => pure #[]
     | some attrs => elabDeclAttrs attrs
   return {
-    docString?, visibility, recKind, attrs,
+    stx, docString?, visibility, recKind, attrs,
     isUnsafe        := !unsafeStx.isNone
     isNoncomputable := !noncompStx.isNone
   }

src/Lean/Elab/Declaration.lean

@@ -104,7 +104,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   let (binders, typeStx) := expandDeclSig stx[2]
   let scopeLevelNames ← getLevelNames
   let ⟨_, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
-  addDeclarationRanges declName stx
+  addDeclarationRanges declName modifiers.stx stx
   runTermElabM fun vars =>
     Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do
       Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration
@@ -144,10 +144,10 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
   let (binders, type?) := expandOptDeclSig decl[2]
   let declId           := decl[1]
   let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
-  addDeclarationRanges declName decl
+  addDeclarationRanges declName modifiers.stx decl
   let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
     -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
-    let mut ctorModifiers ← elabModifiers ctor[2]
+    let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩
     if let some leadingDocComment := ctor[0].getOptional? then
       if ctorModifiers.docString?.isSome then
         logErrorAt leadingDocComment "duplicate doc string"
@@ -214,17 +214,18 @@ def elabDeclaration : CommandElab := fun stx => do
     -- only case implementing incrementality currently
     elabMutualDef #[stx]
   else withoutCommandIncrementality true do
+    let modifiers : TSyntax ``Parser.Command.declModifiers := ⟨stx[0]⟩
     if declKind == ``Lean.Parser.Command.«axiom» then
-      let modifiers ← elabModifiers stx[0]
+      let modifiers ← elabModifiers modifiers
       elabAxiom modifiers decl
     else if declKind == ``Lean.Parser.Command.«inductive» then
-      let modifiers ← elabModifiers stx[0]
+      let modifiers ← elabModifiers modifiers
       elabInductive modifiers decl
     else if declKind == ``Lean.Parser.Command.classInductive then
-      let modifiers ← elabModifiers stx[0]
+      let modifiers ← elabModifiers modifiers
       elabClassInductive modifiers decl
     else if declKind == ``Lean.Parser.Command.«structure» then
-      let modifiers ← elabModifiers stx[0]
+      let modifiers ← elabModifiers modifiers
       elabStructure modifiers decl
     else
       throwError "unexpected declaration"
@@ -238,7 +239,7 @@ private def isMutualInductive (stx : Syntax) : Bool :=
 
 private def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
   let views ← elems.mapM fun stx => do
-     let modifiers ← elabModifiers stx[0]
+     let modifiers ← elabModifiers ⟨stx[0]⟩
      inductiveSyntaxToView modifiers stx[1]
   elabInductiveViews views
 
@@ -399,7 +400,7 @@ def elabMutual : CommandElab := fun stx => do
       -- We need to add `id`'s ranges *before* elaborating `initFn` (and then `id` itself) as
       -- otherwise the info context created by `with_decl_name` will be incomplete and break the
       -- call hierarchy
-      addDeclarationRanges fullId defStx
+      addDeclarationRanges fullId ⟨defStx.raw[0]⟩ defStx.raw[1]
       elabCommand (← `(
         $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
         $defStx:command))

src/Lean/Elab/DeclarationRange.lean

@@ -11,12 +11,14 @@ import Lean.Data.Lsp.Utf16
 
 namespace Lean.Elab
 
-def getDeclarationRange [Monad m] [MonadFileMap m] (stx : Syntax) : m DeclarationRange := do
+def getDeclarationRange? [Monad m] [MonadFileMap m] (stx : Syntax) : m (Option DeclarationRange) := do
+  let some range := stx.getRange?
+    | return none
   let fileMap ← getFileMap
-  let pos    := stx.getPos?.getD 0
-  let endPos := stx.getTailPos?.getD pos |> fileMap.toPosition
-  let pos    := pos |> fileMap.toPosition
-  return {
+  --let range := fileMap.utf8RangeToLspRange
+  let pos    := fileMap.toPosition range.start
+  let endPos := fileMap.toPosition range.stop
+  return some {
     pos          := pos
     charUtf16    := fileMap.leanPosToLspPos pos |>.character
     endPos       := endPos
@@ -49,23 +51,27 @@ def getDeclarationSelectionRef (stx : Syntax) : Syntax :=
 
 
 /--
-  Store the `range` and `selectionRange` for `declName` where `stx` is the whole syntax object describing `declName`.
-  This method is for the builtin declarations only.
-  User-defined commands should use `Lean.addDeclarationRanges` to store this information for their commands. -/
-def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) : m Unit := do
-  if stx.getKind == ``Parser.Command.«example» then
+Stores the `range` and `selectionRange` for `declName` where `modsStx` is the modifier part and
+`cmdStx` the remaining part of the syntax tree for `declName`.
+
+This method is for the builtin declarations only. User-defined commands should use
+`Lean.addDeclarationRanges` to store this information for their commands.
+-/
+def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name)
+    (modsStx : TSyntax ``Parser.Command.declModifiers) (declStx : Syntax) : m Unit := do
+  if declStx.getKind == ``Parser.Command.«example» then
     return ()
-  else
-    Lean.addDeclarationRanges declName {
-      range          := (← getDeclarationRange stx)
-      selectionRange := (← getDeclarationRange (getDeclarationSelectionRef stx))
-    }
+  let stx := mkNullNode #[modsStx, declStx]
+  -- may fail on partial syntax, ignore in that case
+  let some range ← getDeclarationRange? stx | return
+  let some selectionRange ← getDeclarationRange? (getDeclarationSelectionRef declStx) | return
+  Lean.addDeclarationRanges declName { range, selectionRange }
 
 /-- Auxiliary method for recording ranges for auxiliary declarations (e.g., fields, nested declarations, etc. -/
 def addAuxDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) (header : Syntax) : m Unit := do
-  Lean.addDeclarationRanges declName {
-    range          := (← getDeclarationRange stx)
-    selectionRange := (← getDeclarationRange header)
-  }
+  -- may fail on partial syntax, ignore in that case
+  let some range ← getDeclarationRange? stx | return
+  let some selectionRange ← getDeclarationRange? header | return
+  Lean.addDeclarationRanges declName { range, selectionRange }
 
 end Lean.Elab

src/Lean/Elab/MutualDef.lean

@@ -887,6 +887,7 @@ def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind :=
   else DefKind.«def»
 
 def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers := {
+  stx             := ⟨mkNullNode #[]⟩  -- ignore when computing declaration range
   isNoncomputable := mainHeaders.any fun h => h.modifiers.isNoncomputable
   recKind         := if mainHeaders.any fun h => h.modifiers.isPartial then RecKind.partial else RecKind.default
   isUnsafe        := mainHeaders.any fun h => h.modifiers.isUnsafe
@@ -997,7 +998,7 @@ where
       for view in views, header in headers do
         -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
         -- that depends only on a part of the ref
-        addDeclarationRanges header.declName view.ref
+        addDeclarationRanges header.declName view.modifiers.stx view.ref
 
 
   processDeriving (headers : Array DefViewElabHeader) := do
@@ -1021,7 +1022,7 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
     let mut reusedAllHeaders := true
     for h : i in [0:ds.size], headerPromise in headerPromises do
       let d := ds[i]
-      let modifiers ← elabModifiers d[0]
+      let modifiers ← elabModifiers ⟨d[0]⟩
       if ds.size > 1 && modifiers.isNonrec then
         throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
       let mut view ← mkDefView modifiers d[1]

src/Lean/Elab/PreDefinition/Basic.lean

@@ -221,7 +221,7 @@ def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit :=
               else
                 none
             | _ => none
-          modifiers := {} }
+          modifiers := default }
 
 private def containsRecFn (recFnNames : Array Name) (e : Expr) : Bool :=
   (e.find? fun e => e.isConst && recFnNames.contains e.constName!).isSome

src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean

@@ -15,7 +15,7 @@ partial def addSmartUnfoldingDefAux (preDef : PreDefinition) (recArgPos : Nat) :
   return { preDef with
     declName  := mkSmartUnfoldingNameFor preDef.declName
     value     := (← visit preDef.value)
-    modifiers := {}
+    modifiers := default
   }
 where
   /--

src/Lean/Elab/Structure.lean

@@ -95,7 +95,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
     let declName := structDeclName ++ defaultCtorName
     let ref := structStx[1].mkSynthetic
     addAuxDeclarationRanges declName ref ref
-    pure { ref, modifiers := {}, name := defaultCtorName, declName }
+    pure { ref, modifiers := default, name := defaultCtorName, declName }
   if structStx[5].isNone then
     useDefault
   else
@@ -912,7 +912,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
       let scopeLevelNames ← Term.getLevelNames
       let ⟨name, declName, allUserLevelNames⟩ ← Elab.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
       Term.withAutoBoundImplicitForbiddenPred (fun n => name == n) do
-        addDeclarationRanges declName stx
+        addDeclarationRanges declName modifiers.stx stx
         Term.withDeclName declName do
           let ctor ← expandCtor stx modifiers declName
           let fields ← expandFields stx modifiers declName

src/Lean/Elab/Tactic/Ext.lean

@@ -123,9 +123,7 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
           levelParams := info.levelParams
         }
         modifyEnv fun env => addProtected env extName
-        Lean.addDeclarationRanges extName {
-          range := ← getDeclarationRange (← getRef)
-          selectionRange := ← getDeclarationRange (← getRef) }
+        addAuxDeclarationRanges extName (← getRef) (← getRef)
     catch e =>
       throwError m!"\
         Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}"
@@ -163,9 +161,7 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
         -- Only declarations in a namespace can be protected:
         unless extIffName.isAtomic do
           modifyEnv fun env => addProtected env extIffName
-        Lean.addDeclarationRanges extIffName {
-          range := ← getDeclarationRange (← getRef)
-          selectionRange := ← getDeclarationRange (← getRef) }
+        addAuxDeclarationRanges extName (← getRef) (← getRef)
     catch e =>
       throwError m!"\
         Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\

src/Lean/Elab/Term.lean

@@ -914,7 +914,9 @@ private def applyAttributesCore
   Remark: if the declaration has syntax errors, `declName` may be `.anonymous` see issue #4309
   In this case, we skip attribute application.
   -/
-  unless declName == .anonymous do
+  if declName == .anonymous then
+    return
+  withDeclName declName do
     for attr in attrs do
       withRef attr.stx do withLogging do
       let env ← getEnv

tests/lean/docStr.lean.expected.out

@@ -19,7 +19,7 @@ doc string for 'g' is not available
 "Auxiliary declaration used to implement named patterns like `x@h:p`. "
 "Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\nit reduces `A` and continues building the telescope if it is a `forall`.\n\nIf `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.\n"
 Foo :=
-  { range := { pos := { line := 4, column := 0 },
+  { range := { pos := { line := 3, column := 0 },
                charUtf16 := 0,
                endPos := { line := 6, column := 58 },
                endCharUtf16 := 58 },
@@ -46,7 +46,7 @@ Foo.val :=
                         endPos := { line := 6, column := 47 },
                         endCharUtf16 := 47 } }
 myAxiom :=
-  { range := { pos := { line := 9, column := 0 },
+  { range := { pos := { line := 8, column := 0 },
                charUtf16 := 0,
                endPos := { line := 9, column := 19 },
                endCharUtf16 := 19 },
@@ -91,7 +91,7 @@ Boo.y :=
                         endPos := { line := 15, column := 5 },
                         endCharUtf16 := 5 } }
 Tree :=
-  { range := { pos := { line := 18, column := 0 },
+  { range := { pos := { line := 17, column := 0 },
                charUtf16 := 0,
                endPos := { line := 20, column := 56 },
                endCharUtf16 := 56 },
@@ -100,7 +100,7 @@ Tree :=
                         endPos := { line := 18, column := 14 },
                         endCharUtf16 := 14 } }
 Tree.rec :=
-  { range := { pos := { line := 18, column := 0 },
+  { range := { pos := { line := 17, column := 0 },
                charUtf16 := 0,
                endPos := { line := 20, column := 56 },
                endCharUtf16 := 56 },
@@ -109,7 +109,7 @@ Tree.rec :=
                         endPos := { line := 18, column := 14 },
                         endCharUtf16 := 14 } }
 Tree.casesOn :=
-  { range := { pos := { line := 18, column := 0 },
+  { range := { pos := { line := 17, column := 0 },
                charUtf16 := 0,
                endPos := { line := 20, column := 56 },
                endCharUtf16 := 56 },
@@ -136,7 +136,7 @@ Tree.leaf :=
                         endPos := { line := 20, column := 43 },
                         endCharUtf16 := 43 } }
 Bla.test :=
-  { range := { pos := { line := 25, column := 0 },
+  { range := { pos := { line := 24, column := 0 },
                charUtf16 := 0,
                endPos := { line := 31, column := 16 },
                endCharUtf16 := 16 },

tests/lean/interactive/goTo.lean.expected.out

@@ -92,8 +92,7 @@
   {"start": {"line": 38, "character": 26},
    "end": {"line": 38, "character": 38}},
   "targetRange":
-  {"start": {"line": 38, "character": 22},
-   "end": {"line": 40, "character": 78}},
+  {"start": {"line": 38, "character": 0}, "end": {"line": 40, "character": 78}},
   "originSelectionRange":
   {"start": {"line": 43, "character": 7},
    "end": {"line": 43, "character": 11}}}]