def
Lean.Elab.getDeclarationRange
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadFileMap m]
(stx : Lean.Syntax)
:
Equations
- Lean.Elab.getDeclarationRange stx = do let fileMap ← Lean.getFileMap let pos : String.Pos := Option.getD (Lean.Syntax.getPos? stx) 0 let endPos : Lean.Position := Lean.FileMap.toPosition fileMap (Option.getD (Lean.Syntax.getTailPos? stx) pos) let pos : Lean.Position := Lean.FileMap.toPosition fileMap pos pure { pos := pos, charUtf16 := (Lean.FileMap.leanPosToLspPos fileMap pos).character, endPos := endPos, endCharUtf16 := (Lean.FileMap.leanPosToLspPos fileMap endPos).character }
Equations
- Lean.Elab.getDeclarationSelectionRef stx = if Lean.Syntax.isOfKind stx `Lean.Parser.Command.instance = true then if (!Lean.Syntax.isNone (Lean.Syntax.getOp stx 3)) = true then Lean.Syntax.getOp (Lean.Syntax.getOp stx 3) 0 else Lean.Syntax.getOp stx 1 else if Lean.Syntax.isIdent (Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0) = true then Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0 else if Lean.Syntax.isIdent (Lean.Syntax.getOp stx 1) = true then Lean.Syntax.getOp stx 1 else Lean.Syntax.getOp stx 0
def
Lean.Elab.addDeclarationRanges
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadFileMap m]
(declName : Lean.Name)
(stx : Lean.Syntax)
:
m Unit
Equations
- Lean.Elab.addDeclarationRanges declName stx = if (Lean.Syntax.getKind stx == `Lean.Parser.Command.example) = true then pure () else do let a ← Lean.Elab.getDeclarationRange stx let a_1 ← Lean.Elab.getDeclarationRange (Lean.Elab.getDeclarationSelectionRef stx) Lean.addDeclarationRanges declName { range := a, selectionRange := a_1 }
def
Lean.Elab.addAuxDeclarationRanges
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadFileMap m]
(declName : Lean.Name)
(stx : Lean.Syntax)
(header : Lean.Syntax)
:
m Unit
Equations
- Lean.Elab.addAuxDeclarationRanges declName stx header = do let a ← Lean.Elab.getDeclarationRange stx let a_1 ← Lean.Elab.getDeclarationRange header Lean.addDeclarationRanges declName { range := a, selectionRange := a_1 }